Home | Intuitionistic Logic Explorer Theorem List (p. 43 of 129) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfse 4201 | 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 4202 | 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.) |
⊢ E Se 𝐴 | ||
Theorem | frforeq1 4203 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇)) | ||
Theorem | freq1 4204 | Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | ||
Theorem | frforeq2 4205 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇)) | ||
Theorem | freq2 4206 | Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) | ||
Theorem | frforeq3 4207 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇)) | ||
Theorem | nffrfor 4208 | 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 4209 | Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Fr 𝐴 | ||
Theorem | frirrg 4210 | A well-founded relation is irreflexive. This is the case where 𝐴 exists. (Contributed by Jim Kingdon, 21-Sep-2021.) |
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | fr0 4211 | Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.) |
⊢ 𝑅 Fr ∅ | ||
Theorem | frind 4212* | Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝜓) → 𝜑)) & ⊢ (𝜒 → 𝑅 Fr 𝐴) & ⊢ (𝜒 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → 𝜑) | ||
Theorem | efrirr 4213 | 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.) |
⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴) | ||
Theorem | tz7.2 4214 | Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent E Fr 𝐴. (Contributed by NM, 4-May-1994.) |
⊢ ((Tr 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)) | ||
Theorem | nfwe 4215 | Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 We 𝐴 | ||
Theorem | weeq1 4216 | Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) | ||
Theorem | weeq2 4217 | Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵)) | ||
Theorem | wefr 4218 | A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.) |
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) | ||
Theorem | wepo 4219 | A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.) |
⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴) | ||
Theorem | wetrep 4220* | An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.) |
⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) | ||
Theorem | we0 4221 | Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.) |
⊢ 𝑅 We ∅ | ||
Syntax | word 4222 | Extend the definition of a wff to include the ordinal predicate. |
wff Ord 𝐴 | ||
Syntax | con0 4223 | 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.) |
class On | ||
Syntax | wlim 4224 | Extend the definition of a wff to include the limit ordinal predicate. |
wff Lim 𝐴 | ||
Syntax | csuc 4225 | Extend class notation to include the successor function. |
class suc 𝐴 | ||
Definition | df-iord 4226* | 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 4227 instead for naming consistency with set.mm. (New usage is discouraged.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) | ||
Theorem | dford3 4227* | Alias for df-iord 4226. Use it instead of df-iord 4226 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) | ||
Definition | df-on 4228 | Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.) |
⊢ On = {𝑥 ∣ Ord 𝑥} | ||
Definition | df-ilim 4229 | 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 4230 instead for naming consistency with set.mm. (New usage is discouraged.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) | ||
Theorem | dflim2 4230 | Alias for df-ilim 4229. Use it instead of df-ilim 4229 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) | ||
Definition | df-suc 4231 | 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 4272). 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.) |
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | ||
Theorem | ordeq 4232 | Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) | ||
Theorem | elong 4233 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) | ||
Theorem | elon 4234 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ On ↔ Ord 𝐴) | ||
Theorem | eloni 4235 | An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → Ord 𝐴) | ||
Theorem | elon2 4236 | An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.) |
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V)) | ||
Theorem | limeq 4237 | Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) | ||
Theorem | ordtr 4238 | An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
⊢ (Ord 𝐴 → Tr 𝐴) | ||
Theorem | ordelss 4239 | An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | ||
Theorem | trssord 4240 | A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.) |
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴) | ||
Theorem | ordelord 4241 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | ||
Theorem | tron 4242 | The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.) |
⊢ Tr On | ||
Theorem | ordelon 4243 | An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | ||
Theorem | onelon 4244 | An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | ||
Theorem | ordin 4245 | The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵)) | ||
Theorem | onin 4246 | The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On) | ||
Theorem | onelss 4247 | 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.) |
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtr1 4248 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ontr1 4249 | Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | onintss 4250* | 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.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ On → (𝜓 → ∩ {𝑥 ∈ On ∣ 𝜑} ⊆ 𝐴)) | ||
Theorem | ord0 4251 | The empty set is an ordinal class. (Contributed by NM, 11-May-1994.) |
⊢ Ord ∅ | ||
Theorem | 0elon 4252 | The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.) |
⊢ ∅ ∈ On | ||
Theorem | inton 4253 | The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.) |
⊢ ∩ On = ∅ | ||
Theorem | nlim0 4254 | The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ¬ Lim ∅ | ||
Theorem | limord 4255 | A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → Ord 𝐴) | ||
Theorem | limuni 4256 | A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) | ||
Theorem | limuni2 4257 | The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.) |
⊢ (Lim 𝐴 → Lim ∪ 𝐴) | ||
Theorem | 0ellim 4258 | A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
⊢ (Lim 𝐴 → ∅ ∈ 𝐴) | ||
Theorem | limelon 4259 | A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) | ||
Theorem | onn0 4260 | The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.) |
⊢ On ≠ ∅ | ||
Theorem | onm 4261 | The class of all ordinal numbers is inhabited. (Contributed by Jim Kingdon, 6-Mar-2019.) |
⊢ ∃𝑥 𝑥 ∈ On | ||
Theorem | suceq 4262 | Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) | ||
Theorem | elsuci 4263 | Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | elsucg 4264 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc2g 4265 | Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc 4266 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | elsuc2 4267 | Membership in a successor. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)) | ||
Theorem | nfsuc 4268 | Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 suc 𝐴 | ||
Theorem | elelsuc 4269 | Membership in a successor. (Contributed by NM, 20-Jun-1998.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) | ||
Theorem | sucel 4270* | Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.) |
⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))) | ||
Theorem | suc0 4271 | The successor of the empty set. (Contributed by NM, 1-Feb-2005.) |
⊢ suc ∅ = {∅} | ||
Theorem | sucprc 4272 | A proper class is its own successor. (Contributed by NM, 3-Apr-1995.) |
⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴) | ||
Theorem | unisuc 4273 | 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.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴) | ||
Theorem | unisucg 4274 | 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.) |
⊢ (𝐴 ∈ 𝑉 → (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴)) | ||
Theorem | sssucid 4275 | 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.) |
⊢ 𝐴 ⊆ suc 𝐴 | ||
Theorem | sucidg 4276 | Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴) | ||
Theorem | sucid 4277 | 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.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ suc 𝐴 | ||
Theorem | nsuceq0g 4278 | No successor is empty. (Contributed by Jim Kingdon, 14-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ≠ ∅) | ||
Theorem | eqelsuc 4279 | A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵) | ||
Theorem | iunsuc 4280* | Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ suc 𝐴𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶) | ||
Theorem | suctr 4281 | The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.) |
⊢ (Tr 𝐴 → Tr suc 𝐴) | ||
Theorem | trsuc 4282 | 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.) |
⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴) | ||
Theorem | trsucss 4283 | A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.) |
⊢ (Tr 𝐴 → (𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | sucssel 4284 | A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵)) | ||
Theorem | orduniss 4285 | An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.) |
⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴) | ||
Theorem | onordi 4286 | An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ Ord 𝐴 | ||
Theorem | ontrci 4287 | An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ Tr 𝐴 | ||
Theorem | oneli 4288 | A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ On) | ||
Theorem | onelssi 4289 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴) | ||
Theorem | onelini 4290 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴)) | ||
Theorem | oneluni 4291 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴) | ||
Theorem | onunisuci 4292 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ ∪ suc 𝐴 = 𝐴 | ||
Axiom | ax-un 4293* |
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 4295 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 4296. A version using class
notation is uniex 4297.
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 3989), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 264). The union of a class df-uni 3684 should not be confused with the union of two classes df-un 3025. Their relationship is shown in unipr 3697. (Contributed by NM, 23-Dec-1993.) |
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfun 4294* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axun2 4295* | A variant of the Axiom of Union ax-un 4293. 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 4296* | The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦 𝑦 = ∪ 𝑥 | ||
Theorem | uniex 4297 | The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 2647), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ 𝐴 ∈ V | ||
Theorem | vuniex 4298 | The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) |
⊢ ∪ 𝑥 ∈ V | ||
Theorem | uniexg 4299 | The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.) |
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | ||
Theorem | unex 4300 | The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |