Home | Intuitionistic Logic Explorer Theorem List (p. 45 of 139) | < 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 | onordi 4401 | An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
Theorem | ontrci 4402 | An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.) |
Theorem | oneli 4403 | A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.) |
Theorem | onelssi 4404 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
Theorem | onelini 4405 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
Theorem | oneluni 4406 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
Theorem | onunisuci 4407 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
Axiom | ax-un 4408* |
Axiom of Union. An axiom of Intuitionistic Zermelo-Fraenkel set theory.
It states that a set exists that includes the union of a given set
i.e. the
collection of all members of the members of . The
variant axun2 4410 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 4411. A version using class
notation is uniex 4412.
This is Axiom 3 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4100), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 264). The union of a class df-uni 3787 should not be confused with the union of two classes df-un 3118. Their relationship is shown in unipr 3800. (Contributed by NM, 23-Dec-1993.) |
Theorem | zfun 4409* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
Theorem | axun2 4410* | A variant of the Axiom of Union ax-un 4408. For any set , there exists a set whose members are exactly the members of the members of i.e. the union of . Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
Theorem | uniex2 4411* | The Axiom of Union using the standard abbreviation for union. Given any set , its union exists. (Contributed by NM, 4-Jun-2006.) |
Theorem | uniex 4412 | The Axiom of Union in class notation. This says that if is a set i.e. (see isset 2730), then the union of is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.) |
Theorem | vuniex 4413 | The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) |
Theorem | uniexg 4414 | 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 | uniexd 4415 | Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | unex 4416 | The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.) |
Theorem | unexb 4417 | Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.) |
Theorem | unexg 4418 | A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) |
Theorem | tpexg 4419 | An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
Theorem | unisn3 4420* | Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.) |
Theorem | abnexg 4421* | Sufficient condition for a class abstraction to be a proper class. The class can be thought of as an expression in and the abstraction appearing in the statement as the class of values as varies through . Assuming the antecedents, if that class is a set, then so is the "domain" . The converse holds without antecedent, see abrexexg 6081. Note that the second antecedent cannot be translated to since may depend on . In applications, one may take or (see snnex 4423 and pwnex 4424 respectively, proved from abnex 4422, which is a consequence of abnexg 4421 with ). (Contributed by BJ, 2-Dec-2021.) |
Theorem | abnex 4422* | Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 4423 and pwnex 4424. See the comment of abnexg 4421. (Contributed by BJ, 2-May-2021.) |
Theorem | snnex 4423* | The class of all singletons is a proper class. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) |
Theorem | pwnex 4424* | The class of all power sets is a proper class. See also snnex 4423. (Contributed by BJ, 2-May-2021.) |
Theorem | opeluu 4425 | 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 4426* | Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.) |
Theorem | eusv1 4427* | Two ways to express single-valuedness of a class expression . (Contributed by NM, 14-Oct-2010.) |
Theorem | eusvnf 4428* | 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 4429* | Two ways to say that is a set expression that does not depend on . (Contributed by Mario Carneiro, 18-Nov-2016.) |
Theorem | eusv2i 4430* | 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 4431* | Two ways to express single-valuedness of a class expression . (Contributed by Mario Carneiro, 18-Nov-2016.) |
Theorem | eusv2 4432* | 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 4433* | 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 4434* | Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.) |
Theorem | reusv3 4435* | Two ways to express single-valuedness of a class expression . See reusv1 4433 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.) |
Theorem | alxfr 4436* | Transfer universal quantification from a variable to another variable contained in expression . (Contributed by NM, 18-Feb-2007.) |
Theorem | ralxfrd 4437* | 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 4438* | 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 4439* | Transfer universal quantification from a variable to another variable contained in expression . (Contributed by Mario Carneiro, 20-Aug-2014.) |
Theorem | rexxfr2d 4440* | 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 4441* | 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 4442* | Transfer universal quantification from a variable to another variable contained in expression . This proof does not use ralxfrd 4437. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | rexxfr 4443* | 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 4444* | Class builder membership after substituting an expression (containing ) for in the class expression . (Contributed by NM, 16-Jan-2012.) |
Theorem | rabxfr 4445* | Class builder membership after substituting an expression (containing ) for in the class expression . (Contributed by NM, 10-Jun-2005.) |
Theorem | reuhypd 4446* | A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 16-Jan-2012.) |
Theorem | reuhyp 4447* | A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 15-Nov-2004.) |
Theorem | uniexb 4448 | 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 4449 | 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 | elpwpwel 4450 | A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.) |
Theorem | univ 4451 | The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.) |
Theorem | eldifpw 4452 | Membership in a power class difference. (Contributed by NM, 25-Mar-2007.) |
Theorem | op1stb 4453 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by NM, 25-Nov-2003.) |
Theorem | op1stbg 4454 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by Jim Kingdon, 17-Dec-2018.) |
Theorem | iunpw 4455* | 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 | ifelpwung 4456 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) |
Theorem | ifelpwund 4457 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) |
Theorem | ifelpwun 4458 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) |
Theorem | ifexd 4459 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) |
Theorem | ordon 4460 | 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 4461 | 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 4462 | 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 4463 | 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 4464 | The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.) |
Theorem | onun2i 4465 | 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 4466 | 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 4467 | An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
Theorem | onuni 4468 | The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.) |
Theorem | orduni 4469 | The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.) |
Theorem | bm2.5ii 4470* | Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.) |
Theorem | sucexb 4471 | A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.) |
Theorem | sucexg 4472 | The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.) |
Theorem | sucex 4473 | The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
Theorem | ordsucim 4474 | The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 8-Nov-2018.) |
Theorem | suceloni 4475 | 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 4476 | The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 20-Nov-2018.) |
Theorem | sucelon 4477 | The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.) |
Theorem | ordsucss 4478 | The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.) |
Theorem | ordelsuc 4479 | 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 4480 | 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 4481* | The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.) |
Theorem | onsucelsucr 4482 | Membership is inherited by predecessors. The converse, for all ordinals, implies excluded middle, as shown at onsucelsucexmid 4504. However, the converse does hold where is a natural number, as seen at nnsucelsuc 6453. (Contributed by Jim Kingdon, 17-Jul-2019.) |
Theorem | onsucsssucr 4483 | The subclass relationship between two ordinals is inherited by their predecessors. The converse implies excluded middle, as shown at onsucsssucexmid 4501. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.) |
Theorem | sucunielr 4484 | Successor and union. The converse (where is an ordinal) implies excluded middle, as seen at ordsucunielexmid 4505. (Contributed by Jim Kingdon, 2-Aug-2019.) |
Theorem | unon 4485 | The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40. (Contributed by NM, 12-Nov-2003.) |
Theorem | onuniss2 4486* | The union of the ordinal subsets of an ordinal number is that number. (Contributed by Jim Kingdon, 2-Aug-2019.) |
Theorem | limon 4487 | The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.) |
Theorem | ordunisuc2r 4488* | 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 4489 | An ordinal number is a subset of . (Contributed by NM, 11-Aug-1994.) |
Theorem | onsuci 4490 | 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 4491* | 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 4492 | An existence condition which implies an intersection is an ordinal number. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | ordtriexmidlem 4493 | Lemma for decidability and ordinals. The set is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4495 or weak linearity in ordsoexmid 4536) with a proposition . Our lemma states that it is an ordinal number. (Contributed by Jim Kingdon, 28-Jan-2019.) |
Theorem | ordtriexmidlem2 4494* | Lemma for decidability and ordinals. The set is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4495 or weak linearity in ordsoexmid 4536) with a proposition . Our lemma helps connect that set to excluded middle. (Contributed by Jim Kingdon, 28-Jan-2019.) |
Theorem | ordtriexmid 4495* |
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". Also see exmidontri 7189 which is much the same theorem but biconditionalized and using the EXMID notation. (Contributed by Mario Carneiro and Jim Kingdon, 14-Nov-2018.) |
Theorem | ontriexmidim 4496* | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4495. (Contributed by Jim Kingdon, 26-Aug-2024.) |
DECID | ||
Theorem | ordtri2orexmid 4497* | Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.) |
Theorem | 2ordpr 4498 | Version of 2on 6387 with the definition of expanded and expressed in terms of . (Contributed by Jim Kingdon, 29-Aug-2021.) |
Theorem | ontr2exmid 4499* | An ordinal transitivity law which implies excluded middle. (Contributed by Jim Kingdon, 17-Sep-2021.) |
Theorem | ordtri2or2exmidlem 4500* | A set which is if or if is an ordinal. (Contributed by Jim Kingdon, 29-Aug-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |