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