Home | Intuitionistic Logic Explorer Theorem List (p. 42 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | abssexg 4101* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | pwex 4102 | Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.) |
Theorem | snexg 4103 | A singleton whose element exists is a set. The case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.) |
Theorem | snex 4104 | A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | snexprc 4105 | A singleton whose element is a proper class is a set. The case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.) |
Theorem | notnotsnex 4106 | A singleton is never a proper class. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jul-2022.) |
Theorem | p0ex 4107 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
Theorem | pp0ex 4108 | (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |
Theorem | ord3ex 4109 | The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.) |
Theorem | dtruarb 4110* | At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). This theorem asserts the existence of two sets which do not equal each other; compare with dtruex 4469 in which we are given a set and go from there to a set which is not equal to it. (Contributed by Jim Kingdon, 2-Sep-2018.) |
Theorem | pwuni 4111 | A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) |
Theorem | undifexmid 4112* | Union of complementary parts producing the whole and excluded middle. Although special cases such as undifss 3438 and undifdcss 6804 are provable, the full statement implies excluded middle as shown here. (Contributed by Jim Kingdon, 16-Jun-2022.) |
Syntax | wem 4113 | Formula for an abbreviation of excluded middle. |
EXMID | ||
Definition | df-exmid 4114 |
The expression EXMID will be used as a readable shorthand for
any
form of the law of the excluded middle; this is a useful shorthand
largely because it hides statements of the form "for any
proposition" in
a system which can only quantify over sets, not propositions.
To see how this compares with other ways of expressing excluded middle, compare undifexmid 4112 with exmidundif 4124. The former may be more recognizable as excluded middle because it is in terms of propositions, and the proof may be easier to follow for much the same reason (it just has to show and in the the relevant parts of the proof). The latter, however, has the key advantage of being able to prove both directions of the biconditional. To state that excluded middle implies a proposition is hard to do gracefully without EXMID, because there is no way to write a hypothesis for an arbitrary proposition; instead the hypothesis would need to be the particular instance of excluded middle which that proof needs. Or to say it another way, EXMID implies DECID by exmidexmid 4115 but there is no good way to express the converse. This definition and how we use it is easiest to understand (and most appropriate to assign the name "excluded middle" to) if we assume ax-sep 4041, in which case EXMID means that all propositions are decidable (see exmidexmid 4115 and notice that it relies on ax-sep 4041). If we instead work with ax-bdsep 13071, EXMID as defined here means that all bounded propositions are decidable. (Contributed by Mario Carneiro and Jim Kingdon, 18-Jun-2022.) |
EXMID DECID | ||
Theorem | exmidexmid 4115 |
EXMID implies that an arbitrary proposition is decidable. That is,
EXMID captures the usual meaning of excluded middle when stated in terms
of propositions.
To get other propositional statements which are equivalent to excluded middle, combine this with notnotrdc 828, peircedc 899, or condc 838. (Contributed by Jim Kingdon, 18-Jun-2022.) |
EXMID DECID | ||
Theorem | exmid01 4116 | Excluded middle is equivalent to saying any subset of is either or . (Contributed by BJ and Jim Kingdon, 18-Jun-2022.) |
EXMID | ||
Theorem | pwntru 4117 | A slight strengthening of pwtrufal 13181. (Contributed by Mario Carneiro and Jim Kingdon, 12-Sep-2023.) |
Theorem | exmid1dc 4118* | A convenience theorem for proving that something implies EXMID. Think of this as an alternative to using a proposition, as in proofs like undifexmid 4112 or ordtriexmid 4432. In this context can be thought of as "x is true". (Contributed by Jim Kingdon, 21-Nov-2023.) |
DECID EXMID | ||
Theorem | exmidn0m 4119* | Excluded middle is equivalent to any set being empty or inhabited. (Contributed by Jim Kingdon, 5-Mar-2023.) |
EXMID | ||
Theorem | exmidsssn 4120* | Excluded middle is equivalent to the biconditionalized version of sssnr 3675 for sets. (Contributed by Jim Kingdon, 5-Mar-2023.) |
EXMID | ||
Theorem | exmidsssnc 4121* | Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4116 but lets you choose any set as the element of the singleton rather than just . It is similar to exmidsssn 4120 but for a particular set rather than all sets. (Contributed by Jim Kingdon, 29-Jul-2023.) |
EXMID | ||
Theorem | exmid0el 4122 | Excluded middle is equivalent to decidability of being an element of an arbitrary set. (Contributed by Jim Kingdon, 18-Jun-2022.) |
EXMID DECID | ||
Theorem | exmidel 4123* | Excluded middle is equivalent to decidability of membership for two arbitrary sets. (Contributed by Jim Kingdon, 18-Jun-2022.) |
EXMID DECID | ||
Theorem | exmidundif 4124* | Excluded middle is equivalent to every subset having a complement. That is, the union of a subset and its relative complement being the whole set. Although special cases such as undifss 3438 and undifdcss 6804 are provable, the full statement is equivalent to excluded middle as shown here. (Contributed by Jim Kingdon, 18-Jun-2022.) |
EXMID | ||
Theorem | exmidundifim 4125* | Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4124 with an implication rather than a biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.) |
EXMID | ||
Axiom | ax-pr 4126* | The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4044). (Contributed by NM, 14-Nov-2006.) |
Theorem | zfpair2 4127 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 4126. (Contributed by NM, 14-Nov-2006.) |
Theorem | prexg 4128 | The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3628, prprc1 3626, and prprc2 3627. (Contributed by Jim Kingdon, 16-Sep-2018.) |
Theorem | snelpwi 4129 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.) |
Theorem | snelpw 4130 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
Theorem | prelpwi 4131 | A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.) |
Theorem | rext 4132* | A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.) |
Theorem | sspwb 4133 | Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
Theorem | unipw 4134 | A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.) |
Theorem | pwel 4135 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
Theorem | pwtr 4136 | A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.) |
Theorem | ssextss 4137* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
Theorem | ssext 4138* | An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004.) |
Theorem | nssssr 4139* | Negation of subclass relationship. Compare nssr 3152. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | pweqb 4140 | Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
Theorem | intid 4141* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
Theorem | euabex 4142 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
Theorem | mss 4143* | An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | exss 4144* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
Theorem | opexg 4145 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
Theorem | opex 4146 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | otexg 4147 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
Theorem | elop 4148 | An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opi1 4149 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opi2 4150 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opm 4151* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
Theorem | opnzi 4152 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 4151). (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth1 4153 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth 4154 | The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that and are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.) |
Theorem | opthg 4155 | Ordered pair theorem. and are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opthg2 4156 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth2 4157 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
Theorem | otth2 4158 | Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otth 4159 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | eqvinop 4160* | A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
Theorem | copsexg 4161* | Substitution of class for ordered pair . (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | copsex2t 4162* | Closed theorem form of copsex2g 4163. (Contributed by NM, 17-Feb-2013.) |
Theorem | copsex2g 4163* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) |
Theorem | copsex4g 4164* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
Theorem | 0nelop 4165 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqex 4166 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
Theorem | opcom 4167 | An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.) |
Theorem | moop2 4168* | "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqsn 4169 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) |
Theorem | opeqpr 4170 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) |
Theorem | euotd 4171* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
Theorem | uniop 4172 | The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | uniopel 4173 | Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opabid 4174 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | elopab 4175* | Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
Theorem | opelopabsbALT 4176* | The law of concretion in terms of substitutions. Less general than opelopabsb 4177, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | opelopabsb 4177* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
Theorem | brabsb 4178* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
Theorem | opelopabt 4179* | Closed theorem form of opelopab 4188. (Contributed by NM, 19-Feb-2013.) |
Theorem | opelopabga 4180* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | brabga 4181* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab2a 4182* | Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopaba 4183* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | braba 4184* | The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.) |
Theorem | opelopabg 4185* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | brabg 4186* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab2 4187* | Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab 4188* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.) |
Theorem | brab 4189* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) |
Theorem | opelopabaf 4190* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4188 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
Theorem | opelopabf 4191* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4188 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.) |
Theorem | ssopab2 4192 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.) |
Theorem | ssopab2b 4193 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
Theorem | ssopab2i 4194 | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.) |
Theorem | ssopab2dv 4195* | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
Theorem | eqopab2b 4196 | Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | opabm 4197* | Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.) |
Theorem | iunopab 4198* | Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
Theorem | pwin 4199 | The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) |
Theorem | pwunss 4200 | The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |