![]() |
Metamath
Proof Explorer Theorem List (p. 79 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | onsuc 7801 | The successor of an ordinal number is an ordinal number. Closed form of onsuci 7829. Forward implication of onsucb 7807. 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 7802 | Obsolete version of onsuc 7801 as of 30-Nov-2024. (Contributed by NM, 6-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) | ||
Theorem | ordsuc 7803 | A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7727. (Revised by BTernaryTau, 6-Jan-2025.) |
⊢ (Ord 𝐴 ↔ Ord suc 𝐴) | ||
Theorem | ordsucOLD 7804 | Obsolete version of ordsuc 7803 as of 6-Jan-2025. (Contributed by NM, 3-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Ord 𝐴 ↔ Ord suc 𝐴) | ||
Theorem | ordpwsuc 7805 | 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 7806 | 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 7807 | A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc 7801. (Contributed by NM, 9-Sep-2003.) |
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) | ||
Theorem | ordsucss 7808 | 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 7809 | An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ On → 𝐴 ⊊ suc 𝐴) | ||
Theorem | ordelsuc 7810 | 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 7811* | The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.) |
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥}) | ||
Theorem | ordsucelsuc 7812 | 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 7813 | The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵)) | ||
Theorem | ordsucuniel 7814 | 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 7815 | 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 7816 | The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∪ 𝐶) ∈ {𝐵, 𝐶}) | ||
Theorem | ordunel 7817 | 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 7818 | 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 7819 | An ordinal class is a subclass of the successor of its union. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord 𝐴 → 𝐴 ⊆ suc ∪ 𝐴) | ||
Theorem | orduniorsuc 7820 | 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 7821 | 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 7822 | 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 7823* | The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005.) |
⊢ (Ord 𝐴 → ∪ {𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴} = 𝐴) | ||
Theorem | onsucuni2 7824 | 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 7825 | The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995.) |
⊢ (Ord 𝐴 → ∅ ∈ suc 𝐴) | ||
Theorem | limon 7826 | The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.) |
⊢ Lim On | ||
Theorem | onuniorsuc 7827 | 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 7828 | An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ 𝐴 ⊆ On | ||
Theorem | onsuci 7829 | The successor of an ordinal number is an ordinal number. Inference associated with onsuc 7801 and onsucb 7807. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ suc 𝐴 ∈ On | ||
Theorem | onuniorsuciOLD 7830 | Obsolete version of onuniorsuc 7827 as of 11-Jan-2025. (Contributed by NM, 13-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴) | ||
Theorem | onuninsuci 7831* | 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 7834. (Contributed by NM, 18-Feb-2004.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥) | ||
Theorem | onsucssi 7832 | 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 7833 | 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 7834* | 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 7831. (Contributed by NM, 18-Feb-2004.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) | ||
Theorem | ordunisuc2 7835* | An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | ||
Theorem | ordzsl 7836* | 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 7837* | 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 7838* | 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 7839* | An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | ||
Theorem | limsuc 7840 | The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.) |
⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) | ||
Theorem | limsssuc 7841 | A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003.) |
⊢ (Lim 𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) | ||
Theorem | nlimon 7842* | 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 7843* | The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 Lim 𝑥) → Lim ∪ 𝐴) | ||
Theorem | tfi 7844* |
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 7854 or tfinds 7851 for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004.) |
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → 𝐴 = On) | ||
Theorem | tfisg 7845* | A closed form of tfis 7846. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑) | ||
Theorem | tfis 7846* | 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 7847* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfis2 7848* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfis3 7849* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ On → 𝜒) | ||
Theorem | tfisi 7850* | 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 7851* | 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 7852* | 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 7853* | 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 7854* | 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 7855* | 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 7856* | 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 7857 | Extend class notation to include the class of natural numbers. |
class ω | ||
Definition | df-om 7858* |
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 7859 for an alternate definition. Later, when we
assume the
Axiom of Infinity, we show ω is a set in
omex 9640, and ω can
then be defined per dfom3 9644 (the smallest inductive set) and dfom4 9646.
Note: the natural numbers ω are a subset of the ordinal numbers df-on 6367. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-nn 12217) with analogous properties and operations, but they will be different sets. (Contributed by NM, 15-May-1994.) |
⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | ||
Theorem | dfom2 7859 | 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 7842). (Contributed by NM, 1-Nov-2004.) |
⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}} | ||
Theorem | elom 7860* | Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 9645. (Contributed by NM, 15-May-1994.) |
⊢ (𝐴 ∈ ω ↔ (𝐴 ∈ On ∧ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥))) | ||
Theorem | omsson 7861 | Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ω ⊆ On | ||
Theorem | limomss 7862 | 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 7863 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) | ||
Theorem | nnoni 7864 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
⊢ 𝐴 ∈ ω ⇒ ⊢ 𝐴 ∈ On | ||
Theorem | nnord 7865 | A natural number is ordinal. (Contributed by NM, 17-Oct-1995.) |
⊢ (𝐴 ∈ ω → Ord 𝐴) | ||
Theorem | trom 7866 | 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 7867 | 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 7868 | A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) | ||
Theorem | omon 7869 | 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 7870 | Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.) |
⊢ (ω ∈ V → ω ∈ On) | ||
Theorem | nnlim 7871 | A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.) |
⊢ (𝐴 ∈ ω → ¬ Lim 𝐴) | ||
Theorem | omssnlim 7872 | The class of natural numbers is a subclass of the class of non-limit ordinal numbers. Exercise 4 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ω ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥} | ||
Theorem | limom 7873 | Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Theorem 1.23 of [Schloeder] p. 4. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
⊢ Lim ω | ||
Theorem | peano2b 7874 | A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.) |
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω) | ||
Theorem | nnsuc 7875* | A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.) |
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥) | ||
Theorem | omsucne 7876 | A natural number is not the successor of itself. (Contributed by AV, 17-Oct-2023.) |
⊢ (𝐴 ∈ ω → 𝐴 ≠ suc 𝐴) | ||
Theorem | ssnlim 7877* | An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) |
⊢ ((Ord 𝐴 ∧ 𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}) → 𝐴 ⊆ ω) | ||
Theorem | omsinds 7878* | Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015.) (Proof shortened by BJ, 16-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ ω → 𝜒) | ||
Theorem | omsindsOLD 7879* | Obsolete version of omsinds 7878 as of 16-Oct-2024. (Contributed by Scott Fenton, 17-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ ω → 𝜒) | ||
Theorem | omun 7880 | The union of two finite ordinals is a finite ordinal. (Contributed by Scott Fenton, 15-Mar-2025.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∪ 𝐵) ∈ ω) | ||
Theorem | peano1 7881 | Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 7881 through peano5 7886 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. (Contributed by NM, 15-May-1994.) Avoid ax-un 7727. (Revised by BTernaryTau, 29-Nov-2024.) |
⊢ ∅ ∈ ω | ||
Theorem | peano1OLD 7882 | Obsolete version of peano1 7881 as of 29-Nov-2024. (Contributed by NM, 15-May-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∅ ∈ ω | ||
Theorem | peano2 7883 | The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) |
⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω) | ||
Theorem | peano3 7884 | The successor of any natural number is not zero. One of Peano's five postulates for arithmetic. Proposition 7.30(3) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) |
⊢ (𝐴 ∈ ω → suc 𝐴 ≠ ∅) | ||
Theorem | peano4 7885 | Two natural numbers are equal iff their successors are equal, i.e. the successor function is one-to-one. One of Peano's five postulates for arithmetic. Proposition 7.30(4) of [TakeutiZaring] p. 43. (Contributed by NM, 3-Sep-2003.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | peano5 7886* | The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's five postulates for arithmetic. Proposition 7.30(5) of [TakeutiZaring] p. 43, except our proof does not require the Axiom of Infinity. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction step, is derived from this theorem as Theorem findes 7895. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2135, ax-12 2169. (Revised by Gino Giotto, 3-Oct-2024.) |
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) | ||
Theorem | peano5OLD 7887* | Obsolete version of peano5 7886 as of 3-Oct-2024. (Contributed by NM, 18-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) | ||
Theorem | nn0suc 7888* | A natural number is either 0 or a successor. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) | ||
Theorem | find 7889* | The Principle of Finite Induction (mathematical induction). Corollary 7.31 of [TakeutiZaring] p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that 𝐴 is a set of natural numbers, zero belongs to 𝐴, and given any member of 𝐴 the member's successor also belongs to 𝐴. The conclusion is that every natural number is in 𝐴. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Wolf Lammen, 28-May-2024.) |
⊢ (𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) ⇒ ⊢ 𝐴 = ω | ||
Theorem | findOLD 7890* | Obsolete version of find 7889 as of 28-May-2024. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) ⇒ ⊢ 𝐴 = ω | ||
Theorem | finds 7891* | Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. This is Metamath 100 proof #74. (Contributed by NM, 14-Apr-1995.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ω → 𝜏) | ||
Theorem | findsg 7892* | Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. The basis of this version is an arbitrary natural number 𝐵 instead of zero. (Contributed by NM, 16-Sep-1995.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝐵 ∈ ω → 𝜓) & ⊢ (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏) | ||
Theorem | finds2 7893* | Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 29-Nov-2002.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝜏 → 𝜓) & ⊢ (𝑦 ∈ ω → (𝜏 → (𝜒 → 𝜃))) ⇒ ⊢ (𝑥 ∈ ω → (𝜏 → 𝜑)) | ||
Theorem | finds1 7894* | Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 22-Mar-2006.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃)) ⇒ ⊢ (𝑥 ∈ ω → 𝜑) | ||
Theorem | findes 7895 | Finite induction with explicit substitution. The first hypothesis is the basis and the second is the induction step. Theorem Schema 22 of [Suppes] p. 136. See tfindes 7854 for the transfinite version. This is an alternative for Metamath 100 proof #74. (Contributed by Raph Levien, 9-Jul-2003.) |
⊢ [∅ / 𝑥]𝜑 & ⊢ (𝑥 ∈ ω → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) ⇒ ⊢ (𝑥 ∈ ω → 𝜑) | ||
Theorem | dmexg 7896 | The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.) |
⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) | ||
Theorem | rnexg 7897 | The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) |
⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) | ||
Theorem | dmexd 7898 | The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 ∈ V) | ||
Theorem | fndmexd 7899 | If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ V) | ||
Theorem | dmfex 7900 | If a mapping is a set, its domain is a set. (Contributed by NM, 27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹 ∈ 𝐶 ∧ 𝐹:𝐴⟶𝐵) → 𝐴 ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |