Home | Intuitionistic Logic Explorer Theorem List (p. 42 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 | exse 4101 | Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.) |
Se | ||
Theorem | sess1 4102 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
Se Se | ||
Theorem | sess2 4103 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
Se Se | ||
Theorem | seeq1 4104 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
Se Se | ||
Theorem | seeq2 4105 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
Se Se | ||
Theorem | nfse 4106 | Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Se | ||
Theorem | epse 4107 | The epsilon relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the epsilon relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.) |
Se | ||
Theorem | frforeq1 4108 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
FrFor FrFor | ||
Theorem | freq1 4109 | Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.) |
Theorem | frforeq2 4110 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
FrFor FrFor | ||
Theorem | freq2 4111 | Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.) |
Theorem | frforeq3 4112 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
FrFor FrFor | ||
Theorem | nffrfor 4113 | Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
FrFor | ||
Theorem | nffr 4114 | Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | frirrg 4115 | A well-founded relation is irreflexive. This is the case where exists. (Contributed by Jim Kingdon, 21-Sep-2021.) |
Theorem | fr0 4116 | Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.) |
Theorem | frind 4117* | Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.) |
Theorem | efrirr 4118 | Irreflexivity of the epsilon relation: a class founded by epsilon is not a member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
Theorem | tz7.2 4119 | Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent . (Contributed by NM, 4-May-1994.) |
Theorem | nfwe 4120 | Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | weeq1 4121 | Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.) |
Theorem | weeq2 4122 | Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.) |
Theorem | wefr 4123 | A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.) |
Theorem | wepo 4124 | A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.) |
Theorem | wetrep 4125* | An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.) |
Theorem | we0 4126 | Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.) |
Syntax | word 4127 | Extend the definition of a wff to include the ordinal predicate. |
Syntax | con0 4128 | Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.) |
Syntax | wlim 4129 | Extend the definition of a wff to include the limit ordinal predicate. |
Syntax | csuc 4130 | Extend class notation to include the successor function. |
Definition | df-iord 4131* | Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4132 instead for naming consistency with set.mm. (New usage is discouraged.) |
Theorem | dford3 4132* | Alias for df-iord 4131. Use it instead of df-iord 4131 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.) |
Definition | df-on 4133 | Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.) |
Definition | df-ilim 4134 | Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42, and then changes to (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4135 instead for naming consistency with set.mm. (New usage is discouraged.) |
Theorem | dflim2 4135 | Alias for df-ilim 4134. Use it instead of df-ilim 4134 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.) |
Definition | df-suc 4136 | Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4177). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.) |
Theorem | ordeq 4137 | Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.) |
Theorem | elong 4138 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
Theorem | elon 4139 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
Theorem | eloni 4140 | An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.) |
Theorem | elon2 4141 | An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.) |
Theorem | limeq 4142 | Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | ordtr 4143 | An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
Theorem | ordelss 4144 | An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.) |
Theorem | trssord 4145 | A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.) |
Theorem | ordelord 4146 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.) |
Theorem | tron 4147 | The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.) |
Theorem | ordelon 4148 | An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.) |
Theorem | onelon 4149 | An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.) |
Theorem | ordin 4150 | The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.) |
Theorem | onin 4151 | The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.) |
Theorem | onelss 4152 | An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | ordtr1 4153 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
Theorem | ontr1 4154 | Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.) |
Theorem | onintss 4155* | If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.) |
Theorem | ord0 4156 | The empty set is an ordinal class. (Contributed by NM, 11-May-1994.) |
Theorem | 0elon 4157 | The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.) |
Theorem | inton 4158 | The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.) |
Theorem | nlim0 4159 | The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | limord 4160 | A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
Theorem | limuni 4161 | A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.) |
Theorem | limuni2 4162 | The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.) |
Theorem | 0ellim 4163 | A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
Theorem | limelon 4164 | A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
Theorem | onn0 4165 | The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.) |
Theorem | onm 4166 | The class of all ordinal numbers is inhabited. (Contributed by Jim Kingdon, 6-Mar-2019.) |
Theorem | suceq 4167 | Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | elsuci 4168 | Membership in a successor. This one-way implication does not require that either or be sets. (Contributed by NM, 6-Jun-1994.) |
Theorem | elsucg 4169 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) |
Theorem | elsuc2g 4170 | Variant of membership in a successor, requiring that rather than be a set. (Contributed by NM, 28-Oct-2003.) |
Theorem | elsuc 4171 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.) |
Theorem | elsuc2 4172 | Membership in a successor. (Contributed by NM, 15-Sep-2003.) |
Theorem | nfsuc 4173 | Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.) |
Theorem | elelsuc 4174 | Membership in a successor. (Contributed by NM, 20-Jun-1998.) |
Theorem | sucel 4175* | Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.) |
Theorem | suc0 4176 | The successor of the empty set. (Contributed by NM, 1-Feb-2005.) |
Theorem | sucprc 4177 | A proper class is its own successor. (Contributed by NM, 3-Apr-1995.) |
Theorem | unisuc 4178 | A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.) |
Theorem | unisucg 4179 | A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by Jim Kingdon, 18-Aug-2019.) |
Theorem | sssucid 4180 | A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.) |
Theorem | sucidg 4181 | Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
Theorem | sucid 4182 | A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
Theorem | nsuceq0g 4183 | No successor is empty. (Contributed by Jim Kingdon, 14-Oct-2018.) |
Theorem | eqelsuc 4184 | A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.) |
Theorem | iunsuc 4185* | Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
Theorem | suctr 4186 | The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.) |
Theorem | trsuc 4187 | A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Theorem | trsucss 4188 | A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.) |
Theorem | sucssel 4189 | A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.) |
Theorem | orduniss 4190 | An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.) |
Theorem | onordi 4191 | An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
Theorem | ontrci 4192 | An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.) |
Theorem | oneli 4193 | 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 4194 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
Theorem | onelini 4195 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
Theorem | oneluni 4196 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
Theorem | onunisuci 4197 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
Axiom | ax-un 4198* |
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 4200 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 4201. A version using class
notation is uniex 4202.
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 3906), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 257). The union of a class df-uni 3609 should not be confused with the union of two classes df-un 2950. Their relationship is shown in unipr 3622. (Contributed by NM, 23-Dec-1993.) |
Theorem | zfun 4199* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
Theorem | axun2 4200* | A variant of the Axiom of Union ax-un 4198. 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |