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	ordelsuc 7801	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 7802*	The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.)
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥})
Theorem	ordsucelsuc 7803	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 7804	The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵))
Theorem	ordsucuniel 7805	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 7806	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 7807	The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∪ 𝐶) ∈ {𝐵, 𝐶})
Theorem	ordunel 7808	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 7809	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 7810	An ordinal class is a subclass of the successor of its union. (Contributed by NM, 12-Sep-2003.)
⊢ (Ord 𝐴 → 𝐴 ⊆ suc ∪ 𝐴)
Theorem	orduniorsuc 7811	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 7812	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 7813	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 7814*	The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005.)
⊢ (Ord 𝐴 → ∪ {𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴} = 𝐴)
Theorem	onsucuni2 7815	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 7816	The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995.)
⊢ (Ord 𝐴 → ∅ ∈ suc 𝐴)
Theorem	limon 7817	The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.)
⊢ Lim On
Theorem	onuniorsuc 7818	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 7819	An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ 𝐴 ⊆ On
Theorem	onsuci 7820	The successor of an ordinal number is an ordinal number. Inference associated with onsuc 7792 and onsucb 7798. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc 𝐴 ∈ On
Theorem	onuniorsuciOLD 7821	Obsolete version of onuniorsuc 7818 as of 11-Jan-2025. (Contributed by NM, 13-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)
Theorem	onuninsuci 7822*	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 7825. (Contributed by NM, 18-Feb-2004.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Theorem	onsucssi 7823	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 7824	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 7825*	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 7822. (Contributed by NM, 18-Feb-2004.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥))
Theorem	ordunisuc2 7826*	An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	ordzsl 7827*	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 7828*	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 7829*	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 7830*	An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	limsuc 7831	The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.)
⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))
Theorem	limsssuc 7832	A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003.)
⊢ (Lim 𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵))
Theorem	nlimon 7833*	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 7834*	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 7835*	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 7845 or tfinds 7842 for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004.)
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → 𝐴 = On)
Theorem	tfisg 7836*	A closed form of tfis 7837. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑)
Theorem	tfis 7837*	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 7838*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝑥 ∈ On → 𝜑)
Theorem	tfis2 7839*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝑥 ∈ On → 𝜑)
Theorem	tfis3 7840*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ On → 𝜒)
Theorem	tfisi 7841*	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 7842*	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 7843*	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 7844*	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 7845*	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 7846*	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 7847*	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 7848	Extend class notation to include the class of natural numbers.
class ω
Definition	df-om 7849*	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 7850 for an alternate definition. Later, when we assume the Axiom of Infinity, we show ω is a set in omex 9634, and ω can then be defined per dfom3 9638 (the smallest inductive set) and dfom4 9640. Note: the natural numbers ω are a subset of the ordinal numbers df-on 6358. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-nn 12210) with analogous properties and operations, but they will be different sets. (Contributed by NM, 15-May-1994.)
⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
Theorem	dfom2 7850	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 7833). (Contributed by NM, 1-Nov-2004.)
⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}}
Theorem	elom 7851*	Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 9639. (Contributed by NM, 15-May-1994.)
⊢ (𝐴 ∈ ω ↔ (𝐴 ∈ On ∧ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥)))
Theorem	omsson 7852	Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ω ⊆ On
Theorem	limomss 7853	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 7854	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
Theorem	nnoni 7855	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
⊢ 𝐴 ∈ ω    ⇒   ⊢ 𝐴 ∈ On
Theorem	nnord 7856	A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
⊢ (𝐴 ∈ ω → Ord 𝐴)
Theorem	trom 7857	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 7858	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 7859	A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)
Theorem	omon 7860	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 7861	Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.)
⊢ (ω ∈ V → ω ∈ On)
Theorem	nnlim 7862	A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.)
⊢ (𝐴 ∈ ω → ¬ Lim 𝐴)
Theorem	omssnlim 7863	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 7864	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 7865	A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.)
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
Theorem	nnsuc 7866*	A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.)
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
Theorem	omsucne 7867	A natural number is not the successor of itself. (Contributed by AV, 17-Oct-2023.)
⊢ (𝐴 ∈ ω → 𝐴 ≠ suc 𝐴)
Theorem	ssnlim 7868*	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 7869*	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 7870*	Obsolete version of omsinds 7869 as of 16-Oct-2024. (Contributed by Scott Fenton, 17-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ ω → 𝜒)
Theorem	omun 7871	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 7872	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 7872 through peano5 7877 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 7718. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ∅ ∈ ω
Theorem	peano1OLD 7873	Obsolete version of peano1 7872 as of 29-Nov-2024. (Contributed by NM, 15-May-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∅ ∈ ω
Theorem	peano2 7874	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 7875	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 7876	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 7877*	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 7886. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2129, ax-12 2163. (Revised by Gino Giotto, 3-Oct-2024.)
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴)
Theorem	peano5OLD 7878*	Obsolete version of peano5 7877 as of 3-Oct-2024. (Contributed by NM, 18-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴)
Theorem	nn0suc 7879*	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 7880*	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 7881*	Obsolete version of find 7880 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 7882*	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 7883*	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 7884*	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 7885*	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 7886	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 7845 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 7887	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 7888	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 7889	The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 ∈ V)
Theorem	fndmexd 7890	If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 Fn 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ V)
Theorem	dmfex 7891	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 7892	The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.)
⊢ (𝐹 Fn 𝐴 → (𝐴 ∈ V ↔ 𝐹 ∈ V))
Theorem	fdmexb 7893	The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐴 ∈ V ↔ 𝐹 ∈ V))
Theorem	dmfexALT 7894	Alternate proof of dmfex 7891: shorter but using ax-rep 5275. (Contributed by NM, 27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) (Proof shortened by AV, 23-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 ∈ 𝐶 ∧ 𝐹:𝐴⟶𝐵) → 𝐴 ∈ V)
Theorem	dmex 7895	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ dom 𝐴 ∈ V
Theorem	rnex 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, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ran 𝐴 ∈ V
Theorem	iprc 7897	The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set, as in idcn 23083. (Contributed by NM, 1-Jan-2007.)
⊢ ¬ I ∈ V
Theorem	resiexg 7898	The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7208). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)
Theorem	imaexg 7899	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)
Theorem	imaex 7900	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 “ 𝐵) ∈ V