![]() |
Metamath
Proof Explorer Theorem List (p. 65 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ordtri3 6401 | 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 6402 | A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵))) | ||
Theorem | orddisj 6403 | An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.) |
⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅) | ||
Theorem | onfr 6404 | The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7774 (through epweon 7772) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994.) |
⊢ E Fr On | ||
Theorem | onelpss 6405 | Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))) | ||
Theorem | onsseleq 6406 | Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | onelss 6407 | 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 6408 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ordtr2 6409 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ordtr3 6410 | Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014.) (Proof shortened by JJ, 24-Sep-2021.) |
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | ||
Theorem | ontr1 6411 | 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 6412 | Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | onelssex 6413* | Ordinal less than is equivalent to having an ordinal between them. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐶 ↔ ∃𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏)) | ||
Theorem | ordunidif 6414 | 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 6415 | 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 6416* | 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 6417* | 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 6418 | The empty set is an ordinal class. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 11-May-1994.) |
⊢ Ord ∅ | ||
Theorem | 0elon 6419 | 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 6420 | A nonempty ordinal contains the empty set. Lemma 1.10 of [Schloeder] p. 2. (Contributed by NM, 25-Nov-1995.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | on0eln0 6421 | An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.) |
⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | dflim2 6422 | An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) | ||
Theorem | inton 6423 | The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.) |
⊢ ∩ On = ∅ | ||
Theorem | nlim0 6424 | 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 6425 | A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → Ord 𝐴) | ||
Theorem | limuni 6426 | A limit ordinal is its own supremum (union). Lemma 2.13 of [Schloeder] p. 5. (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) | ||
Theorem | limuni2 6427 | The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.) |
⊢ (Lim 𝐴 → Lim ∪ 𝐴) | ||
Theorem | 0ellim 6428 | A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
⊢ (Lim 𝐴 → ∅ ∈ 𝐴) | ||
Theorem | limelon 6429 | A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) | ||
Theorem | onn0 6430 | The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.) |
⊢ On ≠ ∅ | ||
Theorem | suceq 6431 | Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) | ||
Theorem | elsuci 6432 | 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 6433 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc2g 6434 | Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc 6435 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | elsuc2 6436 | Membership in a successor. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)) | ||
Theorem | nfsuc 6437 | Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 suc 𝐴 | ||
Theorem | elelsuc 6438 | Membership in a successor. (Contributed by NM, 20-Jun-1998.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) | ||
Theorem | sucel 6439* | Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.) |
⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))) | ||
Theorem | suc0 6440 | The successor of the empty set. (Contributed by NM, 1-Feb-2005.) |
⊢ suc ∅ = {∅} | ||
Theorem | sucprc 6441 | A proper class is its own successor. (Contributed by NM, 3-Apr-1995.) |
⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴) | ||
Theorem | unisucs 6442 | 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 6444. (Revised by BJ, 28-Dec-2024.) |
⊢ (𝐴 ∈ 𝑉 → ∪ suc 𝐴 = (∪ 𝐴 ∪ 𝐴)) | ||
Theorem | unisucg 6443 | 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 6444. (Revised by BJ, 28-Dec-2024.) |
⊢ (𝐴 ∈ 𝑉 → (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴)) | ||
Theorem | unisuc 6444 | 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 6445 | 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 6446 | 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 6447 | 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 6448 | No successor is empty. (Contributed by NM, 3-Apr-1995.) |
⊢ suc 𝐴 ≠ ∅ | ||
Theorem | eqelsuc 6449 | A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵) | ||
Theorem | iunsuc 6450* | 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 6451 | 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 6452 | 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 6453 | 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 6454 | 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 6455 | A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
Theorem | ordsssuc2 6456 | 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 6457 | 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 6458 | 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 6459 | 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 6460 | 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 6461 | Ordinal derived from its successor. (Contributed by NM, 20-May-1998.) |
⊢ (Ord 𝐴 → 𝐴 = (suc 𝐴 ∖ {𝐴})) | ||
Theorem | orduniss 6462 | An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.) |
⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴) | ||
Theorem | ordtri2or 6463 | A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtri2or2 6464 | A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtri2or3 6465 | A consequence of total ordering for ordinal classes. Similar to ordtri2or2 6464. (Contributed by David Moews, 1-May-2017.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵))) | ||
Theorem | ordelinel 6466 | 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 6467 | Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003.) |
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶))) | ||
Theorem | ordequn 6468 | 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 6469 | 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 6470 | 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 6471 | A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003.) |
⊢ ((𝐴 ⊆ On ∧ Ord 𝐵) → (∪ 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) | ||
Theorem | suc11 6472 | 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 6473 | The union of two ordinals is an ordinal. (Contributed by Scott Fenton, 9-Aug-2024.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On) | ||
Theorem | ontr 6474 | 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 6475 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) Generalize from onunisuci 6485. (Revised by BJ, 28-Dec-2024.) |
⊢ (𝐴 ∈ On → ∪ suc 𝐴 = 𝐴) | ||
Theorem | onordi 6476 | An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ Ord 𝐴 | ||
Theorem | ontrciOLD 6477 | Obsolete version of ontr 6474 as of 28-Dec-2024. (Contributed by NM, 11-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ On ⇒ ⊢ Tr 𝐴 | ||
Theorem | onirri 6478 | 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 6479 | 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 6480 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴) | ||
Theorem | onssneli 6481 | An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴) | ||
Theorem | onssnel2i 6482 | An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ⊆ 𝐴 → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | onelini 6483 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴)) | ||
Theorem | oneluni 6484 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴) | ||
Theorem | onunisuci 6485 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ ∪ suc 𝐴 = 𝐴 | ||
Theorem | onsseli 6486 | Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | onun2i 6487 | The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ On | ||
Theorem | unizlim 6488 | An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴))) | ||
Theorem | on0eqel 6489 | An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.) |
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈ 𝐴)) | ||
Theorem | snsn0non 6490 | The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 7869). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 6491. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ¬ {{∅}} ∈ On | ||
Theorem | onxpdisj 6491 | Ordinal numbers and ordered pairs are disjoint collections. This theorem can be used if we want to extend a set of ordinal numbers or ordered pairs with disjoint elements. See also snsn0non 6490. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (On ∩ (V × V)) = ∅ | ||
Theorem | onnev 6492 | The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2013.) (Proof shortened by Wolf Lammen, 27-May-2024.) |
⊢ On ≠ V | ||
Syntax | cio 6493 | Extend class notation with Russell's definition description binder (inverted iota). |
class (℩𝑥𝜑) | ||
Theorem | iotajust 6494* | Soundness justification theorem for df-iota 6495. (Contributed by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-iota 6495* |
Define Russell's definition description binder, which can be read as
"the unique 𝑥 such that 𝜑", where 𝜑
ordinarily contains
𝑥 as a free variable. Our definition
is meaningful only when there
is exactly one 𝑥 such that 𝜑 is true (see iotaval 6514);
otherwise, it evaluates to the empty set (see iotanul 6521). Russell used
the inverted iota symbol ℩ to represent
the binder.
Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use riotacl2 7386 (or iotacl 6529 for unbounded iota), as demonstrated in the proof of supub 9477. This can be easier than applying riotasbc 7388 or a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} | ||
Theorem | dfiota2 6496* | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
Theorem | nfiota1 6497 | Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥(℩𝑥𝜑) | ||
Theorem | nfiotadw 6498* | Deduction version of nfiotaw 6499. Version of nfiotad 6500 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2365. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓)) | ||
Theorem | nfiotaw 6499* | Bound-variable hypothesis builder for the ℩ class. Version of nfiota 6501 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 23-Aug-2011.) Avoid ax-13 2365. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥(℩𝑦𝜑) | ||
Theorem | nfiotad 6500 | Deduction version of nfiota 6501. Usage of this theorem is discouraged because it depends on ax-13 2365. Use the weaker nfiotadw 6498 when possible. (Contributed by NM, 18-Feb-2013.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |