$( This is the Metamath database iset.mm. $) $( Metamath is a formal language and associated computer program for archiving, verifying, and studying mathematical proofs, created by Norman Dwight Megill (1950--2021). For more information, visit https://us.metamath.org and https://github.com/metamath/set.mm, and feel free to ask questions at https://groups.google.com/g/metamath. $) $( New users may want to read https://us.metamath.org/ileuni/conventions.html to understand the label naming conventions used in iset.mm. See also the Metamath program command "MM> HELP VERIFY MARKUP" for markup conventions. $) $( To break this file into smaller modules, in the Metamath program type "MM> READ iset.mm" followed by "MM> WRITE SOURCE iset.mm / SPLIT". To recombine, omit "/ SPLIT". $) $( The database iset.mm was created by Mario Carneiro on 21-Jan-2015 from a fork of the database set.mm and has been continuously enriched since then (list of contributors below). Many additions and updates included copying entire theorems and sections from set.mm in order to keep some consistency among these databases. $) $( ! #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# Metamath source file for intuitionistic logic and set theory #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# ~~ PUBLIC DOMAIN ~~ This work is waived of all rights, including copyright, according to the CC0 Public Domain Dedication. https://creativecommons.org/publicdomain/zero/1.0/ Currently active maintainers: See the list in the CONTRIBUTING.md file of https://github.com/metamath/set.mm. Contributor list: DA David Abernethy SA Stefan Allan TA Thierry Arnoux JA Juha Arpiainen JB Jonathan Ben-Naim GB Gregory Bush MC Mario Carneiro PC Paul Chapman DF Drahflow AD Adrian Ducourtial GD Georgy Dunaev SF Scott Fenton GG Gino Giotto JGH Jeff Hankins AH Anthony Hart DH David Harvey CH Chen-Pang He JH Jeff Hoffman SJ Szymon Jaroszewicz BJ Benoit Jubin JK Jim Kingdon NRK Noah R Kingdon WL Wolf Lammen GL Gerard Lang BL Brendan Leahy RL Raph Levien FL Frederic Line RFL Roy F. Longton JM Jeff Madsen RM Rodolfo Medina NM Norman Megill JMG Jia Ming MM Mykola Mostovenko MO Mel L. O'Cat SO Stefan O'Rear JO Jason Orendorff JP Josh Purinton SR Steve Rodriguez ATS Andrew Salmon AS Alan Sare ES Eric Schmidt GS Glauco Siliprandi SS Saveliy Skresanov AWS Andrew W Swan JU Jarvin Udandy AV Alexander van der Vekens DAW David A. Wheeler JY Jonathan Yan FZ Fan Zheng JEH James E. Hanson HTML code for accented names: BJ Benoît Jubin GL Gérard Lang FL Frédéric Liné $) $( See "MM> HELP VERIFY MARKUP" for help with modularization tags. $) $( Begin $[ iset-header.mm $] $) $( ! =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Contents of this header =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= * Quick "How To" * Bibliography * Metamath syntax summary * Other notes * Acceptable shorter proofs =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Quick "How To" =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= How to use this file under Windows 95/98/NT/2K/XP/Vista: 1. Download the program metamath.exe per the instructions on the Metamath home page (https://us.metamath.org) and put it in the same directory as this file. 2. In Windows Explorer, double-click on metamath.exe. 3. Type "read iset.mm" and press Enter. 4. Type "help" for a list of help topics, and "help demo" for some command examples. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Bibliography =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Bibliographical references are made by bracketing an identifer in a theorem's comment, such as [RussellWhitehead]. These refer to HTML tags on the following web pages: Logic and set theory - see https://us.metamath.org/mpegif/mmset.html#bib Hilbert space - see https://us.metamath.org/mpegif/mmhil.html#ref A bracketed reference must be preceded by a theorem number, etc. and followed by a page number. See "MM> HELP WRITE BIBLIOGRAPHY" for details. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Metamath syntax summary =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= The HELP LANGUAGE command in the Metamath program will give you a quick overview of Metamath. The specification is found on pp. 92--95 of the Metamath book. The following syntax summary is provided for convenience but may omit some details. A Metamath database (set of one or more ASCII source files) is a sequence of _tokens_, which are normally separated by spaces or line breaks. The only tokens that are built into the Metamath language are those (two-character sequences) beginning with $, shown in the following. These tokens are called _keywords_: $c ... $. - Constant declaration $v ... $. - Variable declaration $d ... $. - Disjoint (distinct) variable restriction