Home | Intuitionistic Logic Explorer Theorem List (p. 43 of 106) | < 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 | uniex2 4201* | The Axiom of Union using the standard abbreviation for union. Given any set , its union exists. (Contributed by NM, 4-Jun-2006.) |
Theorem | uniex 4202 | The Axiom of Union in class notation. This says that if is a set i.e. (see isset 2578), then the union of is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.) |
Theorem | uniexg 4203 | The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent instead of to make the theorem more general and thus shorten some proofs; obviously the universal class constant is one possible substitution for class variable . (Contributed by NM, 25-Nov-1994.) |
Theorem | unex 4204 | The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.) |
Theorem | unexb 4205 | Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.) |
Theorem | unexg 4206 | A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) |
Theorem | tpexg 4207 | An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
Theorem | unisn3 4208* | Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.) |
Theorem | snnex 4209* | The class of all singletons is a proper class. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) |
Theorem | opeluu 4210 | Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) (Revised by Mario Carneiro, 27-Feb-2016.) |
Theorem | uniuni 4211* | Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.) |
Theorem | eusv1 4212* | Two ways to express single-valuedness of a class expression . (Contributed by NM, 14-Oct-2010.) |
Theorem | eusvnf 4213* | Even if is free in , it is effectively bound when is single-valued. (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | eusvnfb 4214* | Two ways to say that is a set expression that does not depend on . (Contributed by Mario Carneiro, 18-Nov-2016.) |
Theorem | eusv2i 4215* | Two ways to express single-valuedness of a class expression . (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 18-Nov-2016.) |
Theorem | eusv2nf 4216* | Two ways to express single-valuedness of a class expression . (Contributed by Mario Carneiro, 18-Nov-2016.) |
Theorem | eusv2 4217* | Two ways to express single-valuedness of a class expression . (Contributed by NM, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
Theorem | reusv1 4218* | Two ways to express single-valuedness of a class expression . (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
Theorem | reusv3i 4219* | Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.) |
Theorem | reusv3 4220* | Two ways to express single-valuedness of a class expression . See reusv1 4218 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.) |
Theorem | alxfr 4221* | Transfer universal quantification from a variable to another variable contained in expression . (Contributed by NM, 18-Feb-2007.) |
Theorem | ralxfrd 4222* | Transfer universal quantification from a variable to another variable contained in expression . (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
Theorem | rexxfrd 4223* | Transfer universal quantification from a variable to another variable contained in expression . (Contributed by FL, 10-Apr-2007.) (Revised by Mario Carneiro, 15-Aug-2014.) |
Theorem | ralxfr2d 4224* | Transfer universal quantification from a variable to another variable contained in expression . (Contributed by Mario Carneiro, 20-Aug-2014.) |
Theorem | rexxfr2d 4225* | Transfer universal quantification from a variable to another variable contained in expression . (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
Theorem | ralxfr 4226* | Transfer universal quantification from a variable to another variable contained in expression . (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) |
Theorem | ralxfrALT 4227* | Transfer universal quantification from a variable to another variable contained in expression . This proof does not use ralxfrd 4222. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | rexxfr 4228* | Transfer existence from a variable to another variable contained in expression . (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) |
Theorem | rabxfrd 4229* | Class builder membership after substituting an expression (containing ) for in the class expression . (Contributed by NM, 16-Jan-2012.) |
Theorem | rabxfr 4230* | Class builder membership after substituting an expression (containing ) for in the class expression . (Contributed by NM, 10-Jun-2005.) |
Theorem | reuhypd 4231* | A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 16-Jan-2012.) |
Theorem | reuhyp 4232* | A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 15-Nov-2004.) |
Theorem | uniexb 4233 | The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.) |
Theorem | pwexb 4234 | The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003.) |
Theorem | univ 4235 | The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.) |
Theorem | eldifpw 4236 | Membership in a power class difference. (Contributed by NM, 25-Mar-2007.) |
Theorem | op1stb 4237 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by NM, 25-Nov-2003.) |
Theorem | op1stbg 4238 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by Jim Kingdon, 17-Dec-2018.) |
Theorem | iunpw 4239* | An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.) |
Theorem | ordon 4240 | The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.) |
Theorem | ssorduni 4241 | The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Theorem | ssonuni 4242 | The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. (Contributed by NM, 1-Nov-2003.) |
Theorem | ssonunii 4243 | The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.) |
Theorem | onun2 4244 | The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.) |
Theorem | onun2i 4245 | The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) (Constructive proof by Jim Kingdon, 25-Jul-2019.) |
Theorem | ordsson 4246 | Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) |
Theorem | onss 4247 | An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
Theorem | onuni 4248 | The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.) |
Theorem | orduni 4249 | The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.) |
Theorem | bm2.5ii 4250* | Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.) |
Theorem | sucexb 4251 | A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.) |
Theorem | sucexg 4252 | The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.) |
Theorem | sucex 4253 | The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
Theorem | ordsucim 4254 | The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 8-Nov-2018.) |
Theorem | suceloni 4255 | The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.) |
Theorem | ordsucg 4256 | The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 20-Nov-2018.) |
Theorem | sucelon 4257 | The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.) |
Theorem | ordsucss 4258 | The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.) |
Theorem | ordelsuc 4259 | A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 29-Nov-2003.) |
Theorem | onsucssi 4260 | A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 16-Sep-1995.) |
Theorem | onsucmin 4261* | The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.) |
Theorem | onsucelsucr 4262 | Membership is inherited by predecessors. The converse, for all ordinals, implies excluded middle, as shown at onsucelsucexmid 4283. However, the converse does hold where is a natural number, as seen at nnsucelsuc 6101. (Contributed by Jim Kingdon, 17-Jul-2019.) |
Theorem | onsucsssucr 4263 | The subclass relationship between two ordinals is inherited by their predecessors. The converse implies excluded middle, as shown at onsucsssucexmid 4280. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.) |
Theorem | sucunielr 4264 | Successor and union. The converse (where is an ordinal) implies excluded middle, as seen at ordsucunielexmid 4284. (Contributed by Jim Kingdon, 2-Aug-2019.) |
Theorem | unon 4265 | The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40. (Contributed by NM, 12-Nov-2003.) |
Theorem | onuniss2 4266* | The union of the ordinal subsets of an ordinal number is that number. (Contributed by Jim Kingdon, 2-Aug-2019.) |
Theorem | limon 4267 | The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.) |
Theorem | ordunisuc2r 4268* | An ordinal which contains the successor of each of its members is equal to its union. (Contributed by Jim Kingdon, 14-Nov-2018.) |
Theorem | onssi 4269 | An ordinal number is a subset of . (Contributed by NM, 11-Aug-1994.) |
Theorem | onsuci 4270 | The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.) |
Theorem | onintonm 4271* | The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.) |
Theorem | onintrab2im 4272 | An existence condition which implies an intersection is an ordinal number. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | ordtriexmidlem 4273 | Lemma for decidability and ordinals. The set is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4275 or weak linearity in ordsoexmid 4314) with a proposition . Our lemma states that it is an ordinal number. (Contributed by Jim Kingdon, 28-Jan-2019.) |
Theorem | ordtriexmidlem2 4274* | Lemma for decidability and ordinals. The set is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4275 or weak linearity in ordsoexmid 4314) with a proposition . Our lemma helps connect that set to excluded middle. (Contributed by Jim Kingdon, 28-Jan-2019.) |
Theorem | ordtriexmid 4275* |
Ordinal trichotomy implies the law of the excluded middle (that is,
decidability of an arbitrary proposition).
This theorem is stated in "Constructive ordinals", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". (Contributed by Mario Carneiro and Jim Kingdon, 14-Nov-2018.) |
Theorem | ordtri2orexmid 4276* | Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.) |
Theorem | 2ordpr 4277 | Version of 2on 6040 with the definition of expanded and expressed in terms of . (Contributed by Jim Kingdon, 29-Aug-2021.) |
Theorem | ontr2exmid 4278* | An ordinal transitivity law which implies excluded middle. (Contributed by Jim Kingdon, 17-Sep-2021.) |
Theorem | ordtri2or2exmidlem 4279* | A set which is if or if is an ordinal. (Contributed by Jim Kingdon, 29-Aug-2021.) |
Theorem | onsucsssucexmid 4280* | The converse of onsucsssucr 4263 implies excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.) |
Theorem | onsucelsucexmidlem1 4281* | Lemma for onsucelsucexmid 4283. (Contributed by Jim Kingdon, 2-Aug-2019.) |
Theorem | onsucelsucexmidlem 4282* | Lemma for onsucelsucexmid 4283. The set appears as in the proof of Theorem 1.3 in [Bauer] p. 483 (see acexmidlema 5531), and similar sets also appear in other proofs that various propositions imply excluded middle, for example in ordtriexmidlem 4273. (Contributed by Jim Kingdon, 2-Aug-2019.) |
Theorem | onsucelsucexmid 4283* | The converse of onsucelsucr 4262 implies excluded middle. On the other hand, if is constrained to be a natural number, instead of an arbitrary ordinal, then the converse of onsucelsucr 4262 does hold, as seen at nnsucelsuc 6101. (Contributed by Jim Kingdon, 2-Aug-2019.) |
Theorem | ordsucunielexmid 4284* | The converse of sucunielr 4264 (where is an ordinal) implies excluded middle. (Contributed by Jim Kingdon, 2-Aug-2019.) |
Theorem | regexmidlemm 4285* | Lemma for regexmid 4288. is inhabited. (Contributed by Jim Kingdon, 3-Sep-2019.) |
Theorem | regexmidlem1 4286* | Lemma for regexmid 4288. If has a minimal element, excluded middle follows. (Contributed by Jim Kingdon, 3-Sep-2019.) |
Theorem | reg2exmidlema 4287* | Lemma for reg2exmid 4289. If has a minimal element (expressed by ), excluded middle follows. (Contributed by Jim Kingdon, 2-Oct-2021.) |
Theorem | regexmid 4288* |
The axiom of foundation implies excluded middle.
By foundation (or regularity), we mean the principle that every inhabited set has an element which is minimal (when arranged by ). The statement of foundation here is taken from Metamath Proof Explorer's ax-reg, and is identical (modulo one unnecessary quantifier) to the statement of foundation in Theorem "Foundation implies instances of EM" of [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". For this reason, IZF does not adopt foundation as an axiom and instead replaces it with ax-setind 4290. (Contributed by Jim Kingdon, 3-Sep-2019.) |
Theorem | reg2exmid 4289* | If any inhabited set has a minimal element (when expressed by ), excluded middle follows. (Contributed by Jim Kingdon, 2-Oct-2021.) |
Axiom | ax-setind 4290* |
Axiom of -Induction
(also known as set induction). An axiom of
Intuitionistic Zermelo-Fraenkel set theory. Axiom 9 of [Crosilla] p.
"Axioms of CZF and IZF". This replaces the Axiom of
Foundation (also
called Regularity) from Zermelo-Fraenkel set theory.
For more on axioms which might be adopted which are incompatible with this axiom (that is, Non-wellfounded Set Theory but in the absence of excluded middle), see Chapter 20 of [AczelRathjen], p. 183. (Contributed by Jim Kingdon, 19-Oct-2018.) |
Theorem | setindel 4291* | -Induction in terms of membership in a class. (Contributed by Mario Carneiro and Jim Kingdon, 22-Oct-2018.) |
Theorem | setind 4292* | Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21. (Contributed by NM, 17-Sep-2003.) |
Theorem | setind2 4293 | Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996). (Contributed by NM, 17-Sep-2003.) |
Theorem | elirr 4294 | No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. (Contributed by NM, 7-Aug-1994.) (Proof rewritten by Mario Carneiro and Jim Kingdon, 26-Nov-2018.) |
Theorem | ordirr 4295 | Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. (Contributed by NM, 2-Jan-1994.) |
Theorem | nordeq 4296 | A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998.) |
Theorem | ordn2lp 4297 | An ordinal class cannot be an element of one of its members. Variant of first part of Theorem 2.2(vii) of [BellMachover] p. 469. (Contributed by NM, 3-Apr-1994.) |
Theorem | orddisj 4298 | An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.) |
Theorem | orddif 4299 | Ordinal derived from its successor. (Contributed by NM, 20-May-1998.) |
Theorem | elirrv 4300 | The membership relation is irreflexive: no set is a member of itself. Theorem 105 of [Suppes] p. 54. (Contributed by NM, 19-Aug-1993.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |