![]() |
Metamath
Proof Explorer Theorem List (p. 79 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ordsson 7801 | 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.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (Ord 𝐴 → 𝐴 ⊆ On) | ||
Theorem | dford5 7802 | A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021.) |
⊢ (Ord 𝐴 ↔ (𝐴 ⊆ On ∧ Tr 𝐴)) | ||
Theorem | onss 7803 | An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | ||
Theorem | predon 7804 | The predecessor of an ordinal under E and On is itself. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by BJ, 16-Oct-2024.) |
⊢ (𝐴 ∈ On → Pred( E , On, 𝐴) = 𝐴) | ||
Theorem | predonOLD 7805 | Obsolete version of predon 7804 as of 16-Oct-2024. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ On → Pred( E , On, 𝐴) = 𝐴) | ||
Theorem | ssonprc 7806 | Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ (𝐴 ⊆ On → (𝐴 ∉ V ↔ ∪ 𝐴 = On)) | ||
Theorem | onuni 7807 | The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On) | ||
Theorem | orduni 7808 | The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord 𝐴 → Ord ∪ 𝐴) | ||
Theorem | onint 7809 | The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴) | ||
Theorem | onint0 7810 | The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ⊆ On → (∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴)) | ||
Theorem | onssmin 7811* | A nonempty class of ordinal numbers has the smallest member. Exercise 9 of [TakeutiZaring] p. 40. (Contributed by NM, 3-Oct-2003.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) | ||
Theorem | onminesb 7812 | If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 29-Sep-2003.) |
⊢ (∃𝑥 ∈ On 𝜑 → [∩ {𝑥 ∈ On ∣ 𝜑} / 𝑥]𝜑) | ||
Theorem | onminsb 7813 | If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses implicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = ∩ {𝑥 ∈ On ∣ 𝜑} → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ On 𝜑 → 𝜓) | ||
Theorem | oninton 7814 | The intersection of a nonempty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by NM, 29-Jan-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ On) | ||
Theorem | onintrab 7815 | The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003.) |
⊢ (∩ {𝑥 ∈ On ∣ 𝜑} ∈ V ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On) | ||
Theorem | onintrab2 7816 | An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003.) |
⊢ (∃𝑥 ∈ On 𝜑 ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On) | ||
Theorem | onnmin 7817 | No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵 ∈ ∩ 𝐴) | ||
Theorem | onnminsb 7818* | An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. 𝜓 is the wff resulting from the substitution of 𝐴 for 𝑥 in wff 𝜑. (Contributed by NM, 9-Nov-2003.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ On → (𝐴 ∈ ∩ {𝑥 ∈ On ∣ 𝜑} → ¬ 𝜓)) | ||
Theorem | oneqmin 7819* | A way to show that an ordinal number equals the minimum of a nonempty 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 | uniordint 7820* | The union of a set of ordinals is equal to the intersection of its upper bounds. Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ⊆ On → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥}) | ||
Theorem | onminex 7821* | If a wff is true for an ordinal number, then there is the smallest ordinal number for which it is true. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Mario Carneiro, 20-Nov-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ On 𝜑 → ∃𝑥 ∈ On (𝜑 ∧ ∀𝑦 ∈ 𝑥 ¬ 𝜓)) | ||
Theorem | sucon 7822 | The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003.) |
⊢ suc On = On | ||
Theorem | sucexb 7823 | A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.) |
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) | ||
Theorem | sucexg 7824 | The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V) | ||
Theorem | sucex 7825 | The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ suc 𝐴 ∈ V | ||
Theorem | onmindif2 7826 | The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed. (Contributed by NM, 20-Nov-2003.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ ∩ (𝐴 ∖ {∩ 𝐴})) | ||
Theorem | ordsuci 7827 | The successor of an ordinal class is an ordinal class. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 6-Jun-1994.) Extract and adapt from a subproof of onsuc 7830. (Revised by BTernaryTau, 6-Jan-2025.) (Proof shortened by BJ, 11-Jan-2025.) |
⊢ (Ord 𝐴 → Ord suc 𝐴) | ||
Theorem | sucexeloni 7828 | If the successor of an ordinal number exists, it is an ordinal number. This variation of onsuc 7830 does not require ax-un 7753. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof shortened by BJ, 11-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉) → suc 𝐴 ∈ On) | ||
Theorem | sucexeloniOLD 7829 | Obsolete version of sucexeloni 7828 as of 6-Jan-2025. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉) → suc 𝐴 ∈ On) | ||
Theorem | onsuc 7830 | The successor of an ordinal number is an ordinal number. Closed form of onsuci 7858. Forward implication of onsucb 7836. Proposition 7.24 of [TakeutiZaring] p. 41. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 6-Jun-1994.) (Proof shortened by BTernaryTau, 30-Nov-2024.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) | ||
Theorem | suceloniOLD 7831 | Obsolete version of onsuc 7830 as of 30-Nov-2024. (Contributed by NM, 6-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) | ||
Theorem | ordsuc 7832 | A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7753. (Revised by BTernaryTau, 6-Jan-2025.) |
⊢ (Ord 𝐴 ↔ Ord suc 𝐴) | ||
Theorem | ordsucOLD 7833 | Obsolete version of ordsuc 7832 as of 6-Jan-2025. (Contributed by NM, 3-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Ord 𝐴 ↔ Ord suc 𝐴) | ||
Theorem | ordpwsuc 7834 | The collection of ordinals in the power class of an ordinal is its successor. (Contributed by NM, 30-Jan-2005.) |
⊢ (Ord 𝐴 → (𝒫 𝐴 ∩ On) = suc 𝐴) | ||
Theorem | onpwsuc 7835 | The collection of ordinal numbers in the power set of an ordinal number is its successor. (Contributed by NM, 19-Oct-2004.) |
⊢ (𝐴 ∈ On → (𝒫 𝐴 ∩ On) = suc 𝐴) | ||
Theorem | onsucb 7836 | A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc 7830. (Contributed by NM, 9-Sep-2003.) |
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) | ||
Theorem | ordsucss 7837 | The successor of an element of an ordinal class is a subset of it. Lemma 1.14 of [Schloeder] p. 2. (Contributed by NM, 21-Jun-1998.) |
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) | ||
Theorem | onpsssuc 7838 | An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ On → 𝐴 ⊊ suc 𝐴) | ||
Theorem | ordelsuc 7839 | 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.) |
⊢ ((𝐴 ∈ 𝐶 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵)) | ||
Theorem | onsucmin 7840* | The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.) |
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥}) | ||
Theorem | ordsucelsuc 7841 | Membership is inherited by successors. Generalization of Exercise 9 of [TakeutiZaring] p. 42. (Contributed by NM, 22-Jun-1998.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)) | ||
Theorem | ordsucsssuc 7842 | The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵)) | ||
Theorem | ordsucuniel 7843 | Given an element 𝐴 of the union of an ordinal 𝐵, suc 𝐴 is an element of 𝐵 itself. (Contributed by Scott Fenton, 28-Mar-2012.) (Proof shortened by Mario Carneiro, 29-May-2015.) |
⊢ (Ord 𝐵 → (𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵)) | ||
Theorem | ordsucun 7844 | The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors. (Contributed by NM, 28-Nov-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → suc (𝐴 ∪ 𝐵) = (suc 𝐴 ∪ suc 𝐵)) | ||
Theorem | ordunpr 7845 | The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∪ 𝐶) ∈ {𝐵, 𝐶}) | ||
Theorem | ordunel 7846 | The maximum of two ordinals belongs to a third if each of them do. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 ∪ 𝐶) ∈ 𝐴) | ||
Theorem | onsucuni 7847 | A class of ordinal numbers is a subclass of the successor of its union. Similar to Proposition 7.26 of [TakeutiZaring] p. 41. (Contributed by NM, 19-Sep-2003.) |
⊢ (𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴) | ||
Theorem | ordsucuni 7848 | An ordinal class is a subclass of the successor of its union. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord 𝐴 → 𝐴 ⊆ suc ∪ 𝐴) | ||
Theorem | orduniorsuc 7849 | An ordinal class is either its union or the successor of its union. If we adopt the view that zero is a limit ordinal, this means every ordinal class is either a limit or a successor. (Contributed by NM, 13-Sep-2003.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)) | ||
Theorem | unon 7850 | The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40. (Contributed by NM, 12-Nov-2003.) |
⊢ ∪ On = On | ||
Theorem | ordunisuc 7851 | An ordinal class is equal to the union of its successor. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (Ord 𝐴 → ∪ suc 𝐴 = 𝐴) | ||
Theorem | orduniss2 7852* | The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005.) |
⊢ (Ord 𝐴 → ∪ {𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴} = 𝐴) | ||
Theorem | onsucuni2 7853 | A successor ordinal is the successor of its union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∈ On ∧ 𝐴 = suc 𝐵) → suc ∪ 𝐴 = 𝐴) | ||
Theorem | 0elsuc 7854 | The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995.) |
⊢ (Ord 𝐴 → ∅ ∈ suc 𝐴) | ||
Theorem | limon 7855 | The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.) |
⊢ Lim On | ||
Theorem | onuniorsuc 7856 | An ordinal number is either its own union (if zero or a limit ordinal) or the successor of its union. (Contributed by NM, 13-Jun-1994.) Put in closed form. (Revised by BJ, 11-Jan-2025.) |
⊢ (𝐴 ∈ On → (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)) | ||
Theorem | onssi 7857 | An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ 𝐴 ⊆ On | ||
Theorem | onsuci 7858 | The successor of an ordinal number is an ordinal number. Inference associated with onsuc 7830 and onsucb 7836. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ suc 𝐴 ∈ On | ||
Theorem | onuniorsuciOLD 7859 | Obsolete version of onuniorsuc 7856 as of 11-Jan-2025. (Contributed by NM, 13-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴) | ||
Theorem | onuninsuci 7860* | An ordinal is equal to its union if and only if it is not the successor of an ordinal. A closed-form generalization of this result is orduninsuc 7863. (Contributed by NM, 18-Feb-2004.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥) | ||
Theorem | onsucssi 7861 | 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.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵) | ||
Theorem | nlimsucg 7862 | A successor is not a limit ordinal. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ 𝑉 → ¬ Lim suc 𝐴) | ||
Theorem | orduninsuc 7863* | An ordinal class is equal to its union if and only if it is not the successor of an ordinal. Closed-form generalization of onuninsuci 7860. (Contributed by NM, 18-Feb-2004.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) | ||
Theorem | ordunisuc2 7864* | An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | ||
Theorem | ordzsl 7865* | An ordinal is zero, a successor ordinal, or a limit ordinal. Remark 1.12 of [Schloeder] p. 2. (Contributed by NM, 1-Oct-2003.) |
⊢ (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) | ||
Theorem | onzsl 7866* | An ordinal number is zero, a successor ordinal, or a limit ordinal number. (Contributed by NM, 1-Oct-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) | ||
Theorem | dflim3 7867* | An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor. (Contributed by NM, 1-Nov-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) | ||
Theorem | dflim4 7868* | An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | ||
Theorem | limsuc 7869 | The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.) |
⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) | ||
Theorem | limsssuc 7870 | A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003.) |
⊢ (Lim 𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) | ||
Theorem | nlimon 7871* | Two ways to express the class of non-limit ordinal numbers. Part of Definition 7.27 of [TakeutiZaring] p. 42, who use the symbol KI for this class. (Contributed by NM, 1-Nov-2004.) |
⊢ {𝑥 ∈ On ∣ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)} = {𝑥 ∈ On ∣ ¬ Lim 𝑥} | ||
Theorem | limuni3 7872* | The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 Lim 𝑥) → Lim ∪ 𝐴) | ||
Theorem | tfi 7873* |
The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring]
p. 39. This principle states that if 𝐴 is a class of ordinal
numbers with the property that every ordinal number included in 𝐴
also belongs to 𝐴, then every ordinal number is in
𝐴.
See Theorem tfindes 7883 or tfinds 7880 for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004.) |
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → 𝐴 = On) | ||
Theorem | tfisg 7874* | A closed form of tfis 7875. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑) | ||
Theorem | tfis 7875* | Transfinite Induction Schema. If all ordinal numbers less than a given number 𝑥 have a property (induction hypothesis), then all ordinal numbers have the property (conclusion). Exercise 25 of [Enderton] p. 200. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 20-Nov-2016.) |
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfis2f 7876* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfis2 7877* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfis3 7878* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ On → 𝜒) | ||
Theorem | tfisi 7879* | A transfinite induction scheme in "implicit" form where the induction is done on an object derived from the object of interest. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ On) & ⊢ ((𝜑 ∧ (𝑅 ∈ On ∧ 𝑅 ⊆ 𝑇) ∧ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆) & ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | tfinds 7880* | Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. Theorem 1.19 of [Schloeder] p. 3. (Contributed by NM, 16-Apr-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ On → (𝜒 → 𝜃)) & ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) ⇒ ⊢ (𝐴 ∈ On → 𝜏) | ||
Theorem | tfindsg 7881* | Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal 𝐵 instead of zero. Remark in [TakeutiZaring] p. 57. (Contributed by NM, 5-Mar-2004.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝐵 ∈ On → 𝜓) & ⊢ (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) & ⊢ (((Lim 𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)) ⇒ ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → 𝜏) | ||
Theorem | tfindsg2 7882* | Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal suc 𝐵 instead of zero. (Contributed by NM, 5-Jan-2005.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = suc 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝐵 ∈ On → 𝜓) & ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ 𝑦) → (𝜒 → 𝜃)) & ⊢ ((Lim 𝑥 ∧ 𝐵 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝜏) | ||
Theorem | tfindes 7883* | Transfinite Induction with explicit substitution. The first hypothesis is the basis, the second is the induction step for successors, and the third is the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 5-Mar-2004.) |
⊢ [∅ / 𝑥]𝜑 & ⊢ (𝑥 ∈ On → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) & ⊢ (Lim 𝑦 → (∀𝑥 ∈ 𝑦 𝜑 → [𝑦 / 𝑥]𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfinds2 7884* | Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of [Suppes] p. 197. The wff 𝜏 is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝜏 → 𝜓) & ⊢ (𝑦 ∈ On → (𝜏 → (𝜒 → 𝜃))) & ⊢ (Lim 𝑥 → (𝜏 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) ⇒ ⊢ (𝑥 ∈ On → (𝜏 → 𝜑)) | ||
Theorem | tfinds3 7885* | Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. (Contributed by NM, 6-Jan-2005.) (Revised by David Abernethy, 21-Jun-2011.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝜂 → 𝜓) & ⊢ (𝑦 ∈ On → (𝜂 → (𝜒 → 𝜃))) & ⊢ (Lim 𝑥 → (𝜂 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) ⇒ ⊢ (𝐴 ∈ On → (𝜂 → 𝜏)) | ||
Syntax | com 7886 | Extend class notation to include the class of natural numbers. |
class ω | ||
Definition | df-om 7887* |
Define the class of natural numbers, which are all ordinal numbers that
are less than every limit ordinal, i.e., all finite ordinals. Our
definition is a variant of the Definition of N of [BellMachover] p. 471.
See dfom2 7888 for an alternate definition. Later, when we
assume the
Axiom of Infinity, we show ω is a set in
omex 9680, and ω can
then be defined per dfom3 9684 (the smallest inductive set) and dfom4 9686.
Note: the natural numbers ω are a subset of the ordinal numbers df-on 6389. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-nn 12264) with analogous properties and operations, but they will be different sets. (Contributed by NM, 15-May-1994.) |
⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | ||
Theorem | dfom2 7888 | An alternate definition of the set of natural numbers ω. Definition 7.28 of [TakeutiZaring] p. 42, who use the symbol KI for the restricted class abstraction of non-limit ordinal numbers (see nlimon 7871). (Contributed by NM, 1-Nov-2004.) |
⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}} | ||
Theorem | elom 7889* | Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 9685. (Contributed by NM, 15-May-1994.) |
⊢ (𝐴 ∈ ω ↔ (𝐴 ∈ On ∧ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥))) | ||
Theorem | omsson 7890 | Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ω ⊆ On | ||
Theorem | limomss 7891 | The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of [TakeutiZaring] p. 44. Remarkably, our proof does not require the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.) |
⊢ (Lim 𝐴 → ω ⊆ 𝐴) | ||
Theorem | nnon 7892 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) | ||
Theorem | nnoni 7893 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
⊢ 𝐴 ∈ ω ⇒ ⊢ 𝐴 ∈ On | ||
Theorem | nnord 7894 | A natural number is ordinal. (Contributed by NM, 17-Oct-1995.) |
⊢ (𝐴 ∈ ω → Ord 𝐴) | ||
Theorem | trom 7895 | The class of finite ordinals ω is a transitive class. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Tr ω | ||
Theorem | ordom 7896 | The class of finite ordinals ω is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. Theorem 1.22 of [Schloeder] p. 3. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Ord ω | ||
Theorem | elnn 7897 | A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) | ||
Theorem | omon 7898 | The class of natural numbers ω is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinal numbers (if we deny the Axiom of Infinity). Remark in [TakeutiZaring] p. 43. (Contributed by NM, 10-May-1998.) |
⊢ (ω ∈ On ∨ ω = On) | ||
Theorem | omelon2 7899 | Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.) |
⊢ (ω ∈ V → ω ∈ On) | ||
Theorem | nnlim 7900 | A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.) |
⊢ (𝐴 ∈ ω → ¬ Lim 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |