P. 64 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6301-6400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	frpoins3g 6301*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ Pred (𝑅, 𝐴, 𝑥)𝜓 → 𝜑))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ∈ 𝐴) → 𝜒)
2.3.13  Well-ordered induction
Theorem	tz6.26 6302*	All nonempty subclasses of a class having a well-ordered set-like relation have minimal elements for that relation. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
Theorem	tz6.26i 6303*	All nonempty subclasses of a class having a well-ordered set-like relation 𝑅 have 𝑅-minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
Theorem	wfi 6304*	The Principle of Well-Ordered Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if 𝐵 is a subclass of a well-ordered class 𝐴 with the property that every element of 𝐵 whose inital segment is included in 𝐴 is itself equal to 𝐴. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵)
Theorem	wfii 6305*	The Principle of Well-Ordered Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if 𝐵 is a subclass of a well-ordered class 𝐴 with the property that every element of 𝐵 whose inital segment is included in 𝐴 is itself equal to 𝐴. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵)) → 𝐴 = 𝐵)
Theorem	wfisg 6306*	Well-Ordered Induction Schema. If a property passes from all elements less than 𝑦 of a well-ordered class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfis 6307*	Well-Ordered Induction Schema. If all elements less than a given set 𝑥 of the well-ordered class 𝐴 have a property (induction hypothesis), then all elements of 𝐴 have that property. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	wfis2fg 6308*	Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfis2f 6309*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	wfis2g 6310*	Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfis2 6311*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	wfis3 6312*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝜒)
2.3.14  Ordinals
Syntax	word 6313	Extend the definition of a wff to include the ordinal predicate.
wff Ord 𝐴
Syntax	con0 6314	Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On
Syntax	wlim 6315	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim 𝐴
Syntax	csuc 6316	Extend class notation to include the successor function.
class suc 𝐴
Definition	df-ord 6317	Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the membership relation. Variant of definition of [BellMachover] p. 468. Some sources will define a notation for ordinal order corresponding to < and ≤ but we just use ∈ and ⊆ respectively. (Contributed by NM, 17-Sep-1993.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
Definition	df-on 6318	Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
⊢ On = {𝑥 ∣ Ord 𝑥}
Definition	df-lim 6319	Define the limit ordinal predicate, which is true for a nonempty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42. See dflim2 6372, dflim3 7786, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
Definition	df-suc 6320	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8455). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Definition 1.4 of [Schloeder] p. 1, similarly. Ordinal natural numbers defined using this successor function and 0 as the empty set are also called von Neumann ordinals; 0 is the empty set {}, 1 is {0, {0}}, 2 is {1, {1}}, and so on. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 6392), so that the successor of any ordinal class is still an ordinal class (ordsuc 7753), simplifying certain proofs. Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
Theorem	ordeq 6321	Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
Theorem	elong 6322	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Theorem	elon 6323	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ On ↔ Ord 𝐴)
Theorem	eloni 6324	An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → Ord 𝐴)
Theorem	elon2 6325	An ordinal number is an ordinal set. Part of Definition 1.2 of [Schloeder] p. 1. (Contributed by NM, 8-Feb-2004.)
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
Theorem	limeq 6326	Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))
Theorem	ordwe 6327	Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → E We 𝐴)
Theorem	ordtr 6328	An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → Tr 𝐴)
Theorem	ordfr 6329	Membership is well-founded on an ordinal class. In other words, an ordinal class is well-founded. (Contributed by NM, 22-Apr-1994.)
⊢ (Ord 𝐴 → E Fr 𝐴)
Theorem	ordelss 6330	An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
Theorem	trssord 6331	A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴)
Theorem	ordirr 6332	No ordinal class is a member of itself. In other words, the membership relation is irreflexive on ordinal classes. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. Theorem 1.9(i) of [Schloeder] p. 1. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.)
⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)
Theorem	nordeq 6333	A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐴 ≠ 𝐵)
Theorem	ordn2lp 6334	An ordinal class cannot be an element of one of its members. Variant of first part of Theorem 2.2(vii) of [BellMachover] p. 469. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
Theorem	tz7.5 6335*	A nonempty subclass of an ordinal class has a minimal element. Proposition 7.5 of [TakeutiZaring] p. 36. (Contributed by NM, 18-Feb-2004.) (Revised by David Abernethy, 16-Mar-2011.)
⊢ ((Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
Theorem	ordelord 6336	An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 23-Apr-1994.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
Theorem	tron 6337	The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
⊢ Tr On
Theorem	ordelon 6338	An element of an ordinal class is an ordinal number. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
Theorem	onelon 6339	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
Theorem	tz7.7 6340	A transitive class belongs to an ordinal class iff it is strictly included in it. Proposition 7.7 of [TakeutiZaring] p. 37. (Contributed by NM, 5-May-1994.)
⊢ ((Ord 𝐴 ∧ Tr 𝐵) → (𝐵 ∈ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)))
Theorem	ordelssne 6341	For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 25-Nov-1995.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)))
Theorem	ordelpss 6342	For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 17-Jun-1998.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	ordsseleq 6343	For ordinal classes, inclusion is equivalent to membership or equality. (Contributed by NM, 25-Nov-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	ordin 6344	The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵))
Theorem	onin 6345	The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On)
Theorem	ordtri3or 6346	A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. Theorem 1.9(iii) of [Schloeder] p. 1. (Contributed by NM, 10-May-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	ordtri1 6347	A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
Theorem	ontri1 6348	A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
Theorem	ordtri2 6349	A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)))
Theorem	ordtri3 6350	A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by JJ, 24-Sep-2021.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴)))
Theorem	ordtri4 6351	A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵)))
Theorem	orddisj 6352	An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.)
⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅)
Theorem	onfr 6353	The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7719 (through epweon 7717) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994.)
⊢ E Fr On
Theorem	onelpss 6354	Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)))
Theorem	onsseleq 6355	Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	onelss 6356	An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	oneltri 6357	The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6346. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵))
Theorem	ordtr1 6358	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ordtr2 6359	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ordtr3 6360	Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014.) (Proof shortened by JJ, 24-Sep-2021.)
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵)))
Theorem	ontr1 6361	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ontr2 6362	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	onelssex 6363*	Ordinal less than is equivalent to having an ordinal between them. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐶 ↔ ∃𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏))
Theorem	ordunidif 6364	The union of an ordinal stays the same if a subset equal to one of its elements is removed. (Contributed by NM, 10-Dec-2004.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴)
Theorem	ordintdif 6365	If 𝐵 is smaller than 𝐴, then it equals the intersection of the difference. Exercise 11 in [TakeutiZaring] p. 44. (Contributed by Andrew Salmon, 14-Nov-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ (𝐴 ∖ 𝐵) ≠ ∅) → 𝐵 = ∩ (𝐴 ∖ 𝐵))
Theorem	onintss 6366*	If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ On → (𝜓 → ∩ {𝑥 ∈ On ∣ 𝜑} ⊆ 𝐴))
Theorem	oneqmini 6367*	A way to show that an ordinal number equals the minimum of a collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection. (Contributed by NM, 14-Nov-2003.)
⊢ (𝐵 ⊆ On → ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) → 𝐴 = ∩ 𝐵))
Theorem	ord0 6368	The empty set is an ordinal class. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 11-May-1994.)
⊢ Ord ∅
Theorem	0elon 6369	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 17-Sep-1993.)
⊢ ∅ ∈ On
Theorem	ord0eln0 6370	A nonempty ordinal contains the empty set. Lemma 1.10 of [Schloeder] p. 2. (Contributed by NM, 25-Nov-1995.)
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	on0eln0 6371	An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.)
⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	dflim2 6372	An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
Theorem	inton 6373	The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
⊢ ∩ On = ∅
Theorem	nlim0 6374	The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ¬ Lim ∅
Theorem	limord 6375	A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
⊢ (Lim 𝐴 → Ord 𝐴)
Theorem	limuni 6376	A limit ordinal is its own supremum (union). Lemma 2.13 of [Schloeder] p. 5. (Contributed by NM, 4-May-1995.)
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)
Theorem	limuni2 6377	The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
⊢ (Lim 𝐴 → Lim ∪ 𝐴)
Theorem	0ellim 6378	A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
⊢ (Lim 𝐴 → ∅ ∈ 𝐴)
Theorem	limelon 6379	A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)
Theorem	onn0 6380	The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.)
⊢ On ≠ ∅
Theorem	suceqd 6381	Deduction associated with suceq 6382. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → suc 𝐴 = suc 𝐵)
Theorem	suceq 6382	Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
Theorem	elsuci 6383	Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. Lemma 1.13 of [Schloeder] p. 2. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	elsucg 6384	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	elsuc2g 6385	Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	elsuc 6386	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	elsuc2 6387	Membership in a successor. (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))
Theorem	nfsuc 6388	Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 suc 𝐴
Theorem	elelsuc 6389	Membership in a successor. (Contributed by NM, 20-Jun-1998.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵)
Theorem	sucel 6390*	Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)))
Theorem	suc0 6391	The successor of the empty set. (Contributed by NM, 1-Feb-2005.)
⊢ suc ∅ = {∅}
Theorem	sucprc 6392	A proper class is its own successor. (Contributed by NM, 3-Apr-1995.)
⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
Theorem	unisucs 6393	The union of the successor of a set is equal to the binary union of that set with its union. (Contributed by NM, 30-Aug-1993.) Extract from unisuc 6395. (Revised by BJ, 28-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → ∪ suc 𝐴 = (∪ 𝐴 ∪ 𝐴))
Theorem	unisucg 6394	A transitive class is equal to the union of its successor, closed form. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.) Generalize from unisuc 6395. (Revised by BJ, 28-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴))
Theorem	unisuc 6395	A transitive class is equal to the union of its successor, inference form. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴)
Theorem	sssucid 6396	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)
⊢ 𝐴 ⊆ suc 𝐴
Theorem	sucidg 6397	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). Lemma 1.7 of [Schloeder] p. 1. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)
Theorem	sucid 6398	A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ suc 𝐴
Theorem	nsuceq0 6399	No successor is empty. (Contributed by NM, 3-Apr-1995.)
⊢ suc 𝐴 ≠ ∅
Theorem	eqelsuc 6400	A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵)