P. 79 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7801-7900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sucon 7801	The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003.)
⊢ suc On = On
Theorem	sucexb 7802	A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.)
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
Theorem	sucexg 7803	The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V)
Theorem	sucex 7804	The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ suc 𝐴 ∈ V
Theorem	onmindif2 7805	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 7806	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 7809. (Revised by BTernaryTau, 6-Jan-2025.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ (Ord 𝐴 → Ord suc 𝐴)
Theorem	sucexeloni 7807	If the successor of an ordinal number exists, it is an ordinal number. This variation of onsuc 7809 does not require ax-un 7735. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉) → suc 𝐴 ∈ On)
Theorem	sucexeloniOLD 7808	Obsolete version of sucexeloni 7807 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 7809	The successor of an ordinal number is an ordinal number. Closed form of onsuci 7837. Forward implication of onsucb 7815. 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 7810	Obsolete version of onsuc 7809 as of 30-Nov-2024. (Contributed by NM, 6-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)
Theorem	ordsuc 7811	A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7735. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
Theorem	ordsucOLD 7812	Obsolete version of ordsuc 7811 as of 6-Jan-2025. (Contributed by NM, 3-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
Theorem	ordpwsuc 7813	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 7814	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 7815	A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc 7809. (Contributed by NM, 9-Sep-2003.)
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)
Theorem	ordsucss 7816	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 7817	An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ On → 𝐴 ⊊ suc 𝐴)
Theorem	ordelsuc 7818	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 7819*	The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.)
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥})
Theorem	ordsucelsuc 7820	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 7821	The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵))
Theorem	ordsucuniel 7822	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 7823	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 7824	The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∪ 𝐶) ∈ {𝐵, 𝐶})
Theorem	ordunel 7825	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 7826	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 7827	An ordinal class is a subclass of the successor of its union. (Contributed by NM, 12-Sep-2003.)
⊢ (Ord 𝐴 → 𝐴 ⊆ suc ∪ 𝐴)
Theorem	orduniorsuc 7828	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 7829	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 7830	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 7831*	The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005.)
⊢ (Ord 𝐴 → ∪ {𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴} = 𝐴)
Theorem	onsucuni2 7832	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 7833	The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995.)
⊢ (Ord 𝐴 → ∅ ∈ suc 𝐴)
Theorem	limon 7834	The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.)
⊢ Lim On
Theorem	onuniorsuc 7835	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 7836	An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ 𝐴 ⊆ On
Theorem	onsuci 7837	The successor of an ordinal number is an ordinal number. Inference associated with onsuc 7809 and onsucb 7815. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc 𝐴 ∈ On
Theorem	onuniorsuciOLD 7838	Obsolete version of onuniorsuc 7835 as of 11-Jan-2025. (Contributed by NM, 13-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)
Theorem	onuninsuci 7839*	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 7842. (Contributed by NM, 18-Feb-2004.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Theorem	onsucssi 7840	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 7841	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 7842*	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 7839. (Contributed by NM, 18-Feb-2004.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥))
Theorem	ordunisuc2 7843*	An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	ordzsl 7844*	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 7845*	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 7846*	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 7847*	An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	limsuc 7848	The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.)
⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))
Theorem	limsssuc 7849	A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003.)
⊢ (Lim 𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵))
Theorem	nlimon 7850*	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 7851*	The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 Lim 𝑥) → Lim ∪ 𝐴)
2.4.3  Transfinite induction
Theorem	tfi 7852*	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 7862 or tfinds 7859 for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004.)
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → 𝐴 = On)
Theorem	tfisg 7853*	A closed form of tfis 7854. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑)
Theorem	tfis 7854*	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 7855*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝑥 ∈ On → 𝜑)
Theorem	tfis2 7856*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝑥 ∈ On → 𝜑)
Theorem	tfis3 7857*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ On → 𝜒)
Theorem	tfisi 7858*	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 7859*	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 7860*	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 7861*	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 7862*	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 7863*	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 7864*	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 → (𝜂 → 𝜏))
2.4.4  The natural numbers (i.e., finite ordinals)
Syntax	com 7865	Extend class notation to include the class of natural numbers.
class ω
Definition	df-om 7866*	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 7867 for an alternate definition. Later, when we assume the Axiom of Infinity, we show ω is a set in omex 9661, and ω can then be defined per dfom3 9665 (the smallest inductive set) and dfom4 9667. Note: the natural numbers ω are a subset of the ordinal numbers df-on 6368. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-nn 12238) with analogous properties and operations, but they will be different sets. (Contributed by NM, 15-May-1994.)
⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
Theorem	dfom2 7867	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 7850). (Contributed by NM, 1-Nov-2004.)
⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}}
Theorem	elom 7868*	Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 9666. (Contributed by NM, 15-May-1994.)
⊢ (𝐴 ∈ ω ↔ (𝐴 ∈ On ∧ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥)))
Theorem	omsson 7869	Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ω ⊆ On
Theorem	limomss 7870	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 7871	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
Theorem	nnoni 7872	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
⊢ 𝐴 ∈ ω    ⇒   ⊢ 𝐴 ∈ On
Theorem	nnord 7873	A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
⊢ (𝐴 ∈ ω → Ord 𝐴)
Theorem	trom 7874	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 7875	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 7876	A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)
Theorem	omon 7877	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 7878	Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.)
⊢ (ω ∈ V → ω ∈ On)
Theorem	nnlim 7879	A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.)
⊢ (𝐴 ∈ ω → ¬ Lim 𝐴)
Theorem	omssnlim 7880	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 7881	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 7882	A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.)
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
Theorem	nnsuc 7883*	A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.)
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
Theorem	omsucne 7884	A natural number is not the successor of itself. (Contributed by AV, 17-Oct-2023.)
⊢ (𝐴 ∈ ω → 𝐴 ≠ suc 𝐴)
Theorem	ssnlim 7885*	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 7886*	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 7887*	Obsolete version of omsinds 7886 as of 16-Oct-2024. (Contributed by Scott Fenton, 17-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ ω → 𝜒)
Theorem	omun 7888	The union of two finite ordinals is a finite ordinal. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∪ 𝐵) ∈ ω)
2.4.5  Peano's postulates
Theorem	peano1 7889	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 7889 through peano5 7894 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 7735. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ∅ ∈ ω
Theorem	peano1OLD 7890	Obsolete version of peano1 7889 as of 29-Nov-2024. (Contributed by NM, 15-May-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∅ ∈ ω
Theorem	peano2 7891	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 7892	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 7893	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 7894*	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 7903. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2130, ax-12 2167. (Revised by Gino Giotto, 3-Oct-2024.)
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴)
Theorem	peano5OLD 7895*	Obsolete version of peano5 7894 as of 3-Oct-2024. (Contributed by NM, 18-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴)
Theorem	nn0suc 7896*	A natural number is either 0 or a successor. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
2.4.6  Finite induction (for finite ordinals)
Theorem	find 7897*	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 7898*	Obsolete version of find 7897 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 7899*	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 7900*	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 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝐵 ∈ ω → 𝜓)    &   ⊢ (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃))    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏)