| Metamath
Proof Explorer Theorem List (p. 65 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | trssord 6401 | A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.) |
| ⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴) | ||
| Theorem | ordirr 6402 | No ordinal class is a member of itself. In other words, the membership relation is irreflexive on ordinal classes. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. Theorem 1.9(i) of [Schloeder] p. 1. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.) |
| ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) | ||
| Theorem | nordeq 6403 | A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐴 ≠ 𝐵) | ||
| Theorem | ordn2lp 6404 | 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.) |
| ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴)) | ||
| Theorem | tz7.5 6405* | A nonempty subclass of an ordinal class has a minimal element. Proposition 7.5 of [TakeutiZaring] p. 36. (Contributed by NM, 18-Feb-2004.) (Revised by David Abernethy, 16-Mar-2011.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅) | ||
| Theorem | ordelord 6406 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 23-Apr-1994.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | ||
| Theorem | tron 6407 | The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.) |
| ⊢ Tr On | ||
| Theorem | ordelon 6408 | An element of an ordinal class is an ordinal number. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | ||
| Theorem | onelon 6409 | An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | ||
| Theorem | tz7.7 6410 | A transitive class belongs to an ordinal class iff it is strictly included in it. Proposition 7.7 of [TakeutiZaring] p. 37. (Contributed by NM, 5-May-1994.) |
| ⊢ ((Ord 𝐴 ∧ Tr 𝐵) → (𝐵 ∈ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴))) | ||
| Theorem | ordelssne 6411 | For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 25-Nov-1995.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))) | ||
| Theorem | ordelpss 6412 | For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 17-Jun-1998.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
| Theorem | ordsseleq 6413 | For ordinal classes, inclusion is equivalent to membership or equality. (Contributed by NM, 25-Nov-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
| Theorem | ordin 6414 | 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 6415 | The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On) | ||
| Theorem | ordtri3or 6416 | A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. Theorem 1.9(iii) of [Schloeder] p. 1. (Contributed by NM, 10-May-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) | ||
| Theorem | ordtri1 6417 | A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) | ||
| Theorem | ontri1 6418 | A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) | ||
| Theorem | ordtri2 6419 | A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) | ||
| Theorem | ordtri3 6420 | A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by JJ, 24-Sep-2021.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴))) | ||
| Theorem | ordtri4 6421 | A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵))) | ||
| Theorem | orddisj 6422 | An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.) |
| ⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅) | ||
| Theorem | onfr 6423 | The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7797 (through epweon 7795) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994.) |
| ⊢ E Fr On | ||
| Theorem | onelpss 6424 | Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))) | ||
| Theorem | onsseleq 6425 | Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
| Theorem | onelss 6426 | 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 6427 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
| ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
| Theorem | ordtr2 6428 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
| Theorem | ordtr3 6429 | Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014.) (Proof shortened by JJ, 24-Sep-2021.) |
| ⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | ||
| Theorem | ontr1 6430 | Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by NM, 11-Aug-1994.) |
| ⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
| Theorem | ontr2 6431 | Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
| Theorem | onelssex 6432* | Ordinal less than is equivalent to having an ordinal between them. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐶 ↔ ∃𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏)) | ||
| Theorem | ordunidif 6433 | The union of an ordinal stays the same if a subset equal to one of its elements is removed. (Contributed by NM, 10-Dec-2004.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴) | ||
| Theorem | ordintdif 6434 | If 𝐵 is smaller than 𝐴, then it equals the intersection of the difference. Exercise 11 in [TakeutiZaring] p. 44. (Contributed by Andrew Salmon, 14-Nov-2011.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ (𝐴 ∖ 𝐵) ≠ ∅) → 𝐵 = ∩ (𝐴 ∖ 𝐵)) | ||
| Theorem | onintss 6435* | 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 | oneqmini 6436* | A way to show that an ordinal number equals the minimum of a collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection. (Contributed by NM, 14-Nov-2003.) |
| ⊢ (𝐵 ⊆ On → ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) → 𝐴 = ∩ 𝐵)) | ||
| Theorem | ord0 6437 | The empty set is an ordinal class. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 11-May-1994.) |
| ⊢ Ord ∅ | ||
| Theorem | 0elon 6438 | The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 17-Sep-1993.) |
| ⊢ ∅ ∈ On | ||
| Theorem | ord0eln0 6439 | A nonempty ordinal contains the empty set. Lemma 1.10 of [Schloeder] p. 2. (Contributed by NM, 25-Nov-1995.) |
| ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
| Theorem | on0eln0 6440 | An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.) |
| ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
| Theorem | dflim2 6441 | An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004.) |
| ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) | ||
| Theorem | inton 6442 | The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.) |
| ⊢ ∩ On = ∅ | ||
| Theorem | nlim0 6443 | 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 6444 | A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
| ⊢ (Lim 𝐴 → Ord 𝐴) | ||
| Theorem | limuni 6445 | A limit ordinal is its own supremum (union). Lemma 2.13 of [Schloeder] p. 5. (Contributed by NM, 4-May-1995.) |
| ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) | ||
| Theorem | limuni2 6446 | The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.) |
| ⊢ (Lim 𝐴 → Lim ∪ 𝐴) | ||
| Theorem | 0ellim 6447 | A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
| ⊢ (Lim 𝐴 → ∅ ∈ 𝐴) | ||
| Theorem | limelon 6448 | A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) | ||
| Theorem | onn0 6449 | The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.) |
| ⊢ On ≠ ∅ | ||
| Theorem | suceq 6450 | Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) | ||
| Theorem | elsuci 6451 | Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. Lemma 1.13 of [Schloeder] p. 2. (Contributed by NM, 6-Jun-1994.) |
| ⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
| Theorem | elsucg 6452 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
| Theorem | elsuc2g 6453 | Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
| Theorem | elsuc 6454 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
| Theorem | elsuc2 6455 | Membership in a successor. (Contributed by NM, 15-Sep-2003.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)) | ||
| Theorem | nfsuc 6456 | Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 suc 𝐴 | ||
| Theorem | elelsuc 6457 | Membership in a successor. (Contributed by NM, 20-Jun-1998.) |
| ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) | ||
| Theorem | sucel 6458* | Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.) |
| ⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))) | ||
| Theorem | suc0 6459 | The successor of the empty set. (Contributed by NM, 1-Feb-2005.) |
| ⊢ suc ∅ = {∅} | ||
| Theorem | sucprc 6460 | A proper class is its own successor. (Contributed by NM, 3-Apr-1995.) |
| ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴) | ||
| Theorem | unisucs 6461 | The union of the successor of a set is equal to the binary union of that set with its union. (Contributed by NM, 30-Aug-1993.) Extract from unisuc 6463. (Revised by BJ, 28-Dec-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → ∪ suc 𝐴 = (∪ 𝐴 ∪ 𝐴)) | ||
| Theorem | unisucg 6462 | A transitive class is equal to the union of its successor, closed form. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.) Generalize from unisuc 6463. (Revised by BJ, 28-Dec-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴)) | ||
| Theorem | unisuc 6463 | A transitive class is equal to the union of its successor, inference form. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴) | ||
| Theorem | sssucid 6464 | 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 6465 | Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). Lemma 1.7 of [Schloeder] p. 1. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴) | ||
| Theorem | sucid 6466 | 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 | nsuceq0 6467 | No successor is empty. (Contributed by NM, 3-Apr-1995.) |
| ⊢ suc 𝐴 ≠ ∅ | ||
| Theorem | eqelsuc 6468 | A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵) | ||
| Theorem | iunsuc 6469* | 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 6470 | The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.) (Proof shortened by JJ, 24-Sep-2021.) |
| ⊢ (Tr 𝐴 → Tr suc 𝐴) | ||
| Theorem | trsuc 6471 | 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 6472 | A member of the successor of a transitive class is a subclass of it. Lemma 1.13 of [Schloeder] p. 2. (Contributed by NM, 4-Oct-2003.) |
| ⊢ (Tr 𝐴 → (𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴)) | ||
| Theorem | ordsssuc 6473 | An ordinal is a subset of another ordinal if and only if it belongs to its successor. (Contributed by NM, 28-Nov-2003.) |
| ⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
| Theorem | onsssuc 6474 | A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
| Theorem | ordsssuc2 6475 | An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
| Theorem | onmindif 6476 | When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. (Contributed by NM, 1-Dec-2003.) |
| ⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ On) → 𝐵 ∈ ∩ (𝐴 ∖ suc 𝐵)) | ||
| Theorem | ordnbtwn 6477 | There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of [TakeutiZaring] p. 41. Lemma 1.15 of [Schloeder] p. 2. (Contributed by NM, 21-Jun-1998.) (Proof shortened by JJ, 24-Sep-2021.) |
| ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | ||
| Theorem | onnbtwn 6478 | There is no set between an ordinal number and its successor. Proposition 7.25 of [TakeutiZaring] p. 41. Lemma 1.15 of [Schloeder] p. 2. (Contributed by NM, 9-Jun-1994.) |
| ⊢ (𝐴 ∈ On → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | ||
| Theorem | sucssel 6479 | A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.) |
| ⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵)) | ||
| Theorem | orddif 6480 | Ordinal derived from its successor. (Contributed by NM, 20-May-1998.) |
| ⊢ (Ord 𝐴 → 𝐴 = (suc 𝐴 ∖ {𝐴})) | ||
| Theorem | orduniss 6481 | An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.) |
| ⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴) | ||
| Theorem | ordtri2or 6482 | A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
| Theorem | ordtri2or2 6483 | A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
| Theorem | ordtri2or3 6484 | A consequence of total ordering for ordinal classes. Similar to ordtri2or2 6483. (Contributed by David Moews, 1-May-2017.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵))) | ||
| Theorem | ordelinel 6485 | The intersection of two ordinal classes is an element of a third if and only if either one of them is. (Contributed by David Moews, 1-May-2017.) (Proof shortened by JJ, 24-Sep-2021.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → ((𝐴 ∩ 𝐵) ∈ 𝐶 ↔ (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶))) | ||
| Theorem | ordssun 6486 | Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003.) |
| ⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶))) | ||
| Theorem | ordequn 6487 | The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of [TakeutiZaring] p. 40. (Contributed by NM, 28-Nov-2003.) |
| ⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 = (𝐵 ∪ 𝐶) → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | ||
| Theorem | ordun 6488 | The maximum (i.e., union) of two ordinals is ordinal. Exercise 12 of [TakeutiZaring] p. 40. (Contributed by NM, 28-Nov-2003.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∪ 𝐵)) | ||
| Theorem | onunel 6489 | The union of two ordinals is in a third iff both of the first two are. (Contributed by Scott Fenton, 10-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∪ 𝐵) ∈ 𝐶 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶))) | ||
| Theorem | ordunisssuc 6490 | A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003.) |
| ⊢ ((𝐴 ⊆ On ∧ Ord 𝐵) → (∪ 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) | ||
| Theorem | suc11 6491 | The successor operation behaves like a one-to-one function. Compare Exercise 16 of [Enderton] p. 194. (Contributed by NM, 3-Sep-2003.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | onun2 6492 | The union of two ordinals is an ordinal. (Contributed by Scott Fenton, 9-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On) | ||
| Theorem | ontr 6493 | An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.) Put in closed form. (Resised by BJ, 28-Dec-2024.) |
| ⊢ (𝐴 ∈ On → Tr 𝐴) | ||
| Theorem | onunisuc 6494 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) Generalize from onunisuci 6504. (Revised by BJ, 28-Dec-2024.) |
| ⊢ (𝐴 ∈ On → ∪ suc 𝐴 = 𝐴) | ||
| Theorem | onordi 6495 | An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ Ord 𝐴 | ||
| Theorem | ontrciOLD 6496 | Obsolete version of ontr 6493 as of 28-Dec-2024. (Contributed by NM, 11-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ Tr 𝐴 | ||
| Theorem | onirri 6497 | An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ ¬ 𝐴 ∈ 𝐴 | ||
| Theorem | oneli 6498 | 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 6499 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴) | ||
| Theorem | onssneli 6500 | An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |