P. 78 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7701-7800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tpex 7701	An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)
⊢ {𝐴, 𝐵, 𝐶} ∈ V
Theorem	unexb 7702	Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
Theorem	unexbOLD 7703	Obsolete version of unexb 7702 as of 21-Jul-2025. (Contributed by NM, 11-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
Theorem	unexgOLD 7704	Obsolete version of unexg 7698 as of 21-Jul-2025. (Contributed by NM, 18-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	xpexg 7705	The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7935. (Contributed by NM, 14-Aug-1994.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
Theorem	xpexd 7706	The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
Theorem	3xpexg 7707	The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
⊢ (𝑉 ∈ 𝑊 → ((𝑉 × 𝑉) × 𝑉) ∈ V)
Theorem	xpex 7708	The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 × 𝐵) ∈ V
Theorem	unexd 7709	The union of two sets is a set. (Contributed by SN, 16-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)
Theorem	sqxpexg 7710	The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)
Theorem	abnexg 7711*	Sufficient condition for a class abstraction to be a proper class. The class 𝐹 can be thought of as an expression in 𝑥 and the abstraction appearing in the statement as the class of values 𝐹 as 𝑥 varies through 𝐴. Assuming the antecedents, if that class is a set, then so is the "domain" 𝐴. The converse holds without antecedent, see abrexexg 7915. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 7713 and pwnex 7714 respectively, proved from abnex 7712, which is a consequence of abnexg 7711 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.)
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V))
Theorem	abnex 7712*	Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 7713 and pwnex 7714. See the comment of abnexg 7711. (Contributed by BJ, 2-May-2021.)
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V)
Theorem	snnex 7713*	The class of all singletons is a proper class. See also pwnex 7714. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof shortened by BJ, 5-Dec-2021.)
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V
Theorem	pwnex 7714*	The class of all power sets is a proper class. See also snnex 7713. (Contributed by BJ, 2-May-2021.)
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V
Theorem	difex2 7715	If the subtrahend of a class difference exists, then the minuend exists iff the difference exists. (Contributed by NM, 12-Nov-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ V ↔ (𝐴 ∖ 𝐵) ∈ V))
Theorem	difsnexi 7716	If the difference of a class and a singleton is a set, the class itself is a set. (Contributed by AV, 15-Jan-2019.)
⊢ ((𝑁 ∖ {𝐾}) ∈ V → 𝑁 ∈ V)
Theorem	uniuni 7717*	Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007.)
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)}
Theorem	uniexr 7718	Converse of the Axiom of Union. Note that it does not require ax-un 7690. (Contributed by NM, 11-Nov-2003.)
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V)
Theorem	uniexb 7719	The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.)
⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V)
Theorem	pwexr 7720	Converse of the Axiom of Power Sets. Note that it does not require ax-pow 5312. (Contributed by NM, 11-Nov-2003.)
⊢ (𝒫 𝐴 ∈ 𝑉 → 𝐴 ∈ V)
Theorem	pwexb 7721	The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003.)
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
Theorem	elpwpwel 7722	A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.)
⊢ (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵)
Theorem	eldifpw 7723	Membership in a power class difference. (Contributed by NM, 25-Mar-2007.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵))
Theorem	elpwun 7724	Membership in the power class of a union. (Contributed by NM, 26-Mar-2007.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝒫 (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐶) ∈ 𝒫 𝐵)
Theorem	pwuncl 7725	Power classes are closed under union. (Contributed by AV, 27-Feb-2024.)
⊢ ((𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋) → (𝐴 ∪ 𝐵) ∈ 𝒫 𝑋)
Theorem	iunpw 7726*	An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥)
Theorem	fr3nr 7727	A well-founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 10-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵))
Theorem	epne3 7728	A well-founded class contains no 3-cycle loops. (Contributed by NM, 19-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
⊢ (( E Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐵))
Theorem	dfwe2 7729*	Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
2.4.2  Ordinals (continued)
Theorem	epweon 7730	The membership relation well-orders the class of ordinal numbers. This proof does not require the axiom of regularity. Proposition 4.8(g) of [Mendelson] p. 244. For a shorter proof requiring ax-un 7690, see epweonALT 7731. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7690. (Revised by BTernaryTau, 30-Nov-2024.)
⊢ E We On
Theorem	epweonALT 7731	Alternate proof of epweon 7730, shorter but requiring ax-un 7690. (Contributed by NM, 1-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ E We On
Theorem	ordon 7732	The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.)
⊢ Ord On
Theorem	onprc 7733	No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. This is also known as the Burali-Forti paradox (remark in [Enderton] p. 194). In 1897, Cesare Burali-Forti noticed that since the "set" of all ordinal numbers is an ordinal class (ordon 7732), it must be both an element of the set of all ordinal numbers yet greater than every such element. ZF set theory resolves this paradox by not allowing the class of all ordinal numbers to be a set (so instead it is a proper class). Here we prove the denial of its existence. (Contributed by NM, 18-May-1994.)
⊢ ¬ On ∈ V
Theorem	ssorduni 7734	The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. Lemma 2.7 of [Schloeder] p. 4. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴)
Theorem	ssonuni 7735	The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. Lemma 2.7 of [Schloeder] p. 4. (Contributed by NM, 1-Nov-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊆ On → ∪ 𝐴 ∈ On))
Theorem	ssonunii 7736	The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ⊆ On → ∪ 𝐴 ∈ On)
Theorem	ordeleqon 7737	A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of [TakeutiZaring] p. 38 and its converse. (Contributed by NM, 1-Jun-2003.)
⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
Theorem	ordsson 7738	Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ (Ord 𝐴 → 𝐴 ⊆ On)
Theorem	dford5 7739	A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021.)
⊢ (Ord 𝐴 ↔ (𝐴 ⊆ On ∧ Tr 𝐴))
Theorem	onss 7740	An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
Theorem	predon 7741	The predecessor of an ordinal under E and On is itself. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ (𝐴 ∈ On → Pred( E , On, 𝐴) = 𝐴)
Theorem	ssonprc 7742	Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ⊆ On → (𝐴 ∉ V ↔ ∪ 𝐴 = On))
Theorem	onuni 7743	The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On)
Theorem	orduni 7744	The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.)
⊢ (Ord 𝐴 → Ord ∪ 𝐴)
Theorem	onint 7745	The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴)
Theorem	onint0 7746	The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ⊆ On → (∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴))
Theorem	onssmin 7747*	A nonempty class of ordinal numbers has the smallest member. Exercise 9 of [TakeutiZaring] p. 40. (Contributed by NM, 3-Oct-2003.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)
Theorem	onminesb 7748	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 29-Sep-2003.)
⊢ (∃𝑥 ∈ On 𝜑 → [∩ {𝑥 ∈ On ∣ 𝜑} / 𝑥]𝜑)
Theorem	onminsb 7749	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses implicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ∩ {𝑥 ∈ On ∣ 𝜑} → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ On 𝜑 → 𝜓)
Theorem	oninton 7750	The intersection of a nonempty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by NM, 29-Jan-1997.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ On)
Theorem	onintrab 7751	The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003.)
⊢ (∩ {𝑥 ∈ On ∣ 𝜑} ∈ V ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On)
Theorem	onintrab2 7752	An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003.)
⊢ (∃𝑥 ∈ On 𝜑 ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On)
Theorem	onnmin 7753	No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997.)
⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵 ∈ ∩ 𝐴)
Theorem	onnminsb 7754*	An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. 𝜓 is the wff resulting from the substitution of 𝐴 for 𝑥 in wff 𝜑. (Contributed by NM, 9-Nov-2003.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ On → (𝐴 ∈ ∩ {𝑥 ∈ On ∣ 𝜑} → ¬ 𝜓))
Theorem	oneqmin 7755*	A way to show that an ordinal number equals the minimum of a nonempty 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	uniordint 7756*	The union of a set of ordinals is equal to the intersection of its upper bounds. Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ⊆ On → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	onminex 7757*	If a wff is true for an ordinal number, then there is the smallest ordinal number for which it is true. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Mario Carneiro, 20-Nov-2016.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ On 𝜑 → ∃𝑥 ∈ On (𝜑 ∧ ∀𝑦 ∈ 𝑥 ¬ 𝜓))
Theorem	sucon 7758	The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003.)
⊢ suc On = On
Theorem	sucexb 7759	A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.)
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
Theorem	sucexg 7760	The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V)
Theorem	sucex 7761	The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ suc 𝐴 ∈ V
Theorem	onmindif2 7762	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 7763	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 7765. (Revised by BTernaryTau, 6-Jan-2025.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ (Ord 𝐴 → Ord suc 𝐴)
Theorem	sucexeloni 7764	If the successor of an ordinal number exists, it is an ordinal number. This variation of onsuc 7765 does not require ax-un 7690. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉) → suc 𝐴 ∈ On)
Theorem	onsuc 7765	The successor of an ordinal number is an ordinal number. Closed form of onsuci 7791. Forward implication of onsucb 7769. 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	ordsuc 7766	A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7690. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
Theorem	ordpwsuc 7767	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 7768	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 7769	A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc 7765. (Contributed by NM, 9-Sep-2003.)
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)
Theorem	ordsucss 7770	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 7771	An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ On → 𝐴 ⊊ suc 𝐴)
Theorem	ordelsuc 7772	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 7773*	The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.)
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥})
Theorem	ordsucelsuc 7774	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 7775	The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵))
Theorem	ordsucuniel 7776	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 7777	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 7778	The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∪ 𝐶) ∈ {𝐵, 𝐶})
Theorem	ordunel 7779	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 7780	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 7781	An ordinal class is a subclass of the successor of its union. (Contributed by NM, 12-Sep-2003.)
⊢ (Ord 𝐴 → 𝐴 ⊆ suc ∪ 𝐴)
Theorem	orduniorsuc 7782	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 7783	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 7784	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 7785*	The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005.)
⊢ (Ord 𝐴 → ∪ {𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴} = 𝐴)
Theorem	onsucuni2 7786	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 7787	The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995.)
⊢ (Ord 𝐴 → ∅ ∈ suc 𝐴)
Theorem	limon 7788	The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.)
⊢ Lim On
Theorem	onuniorsuc 7789	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 7790	An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ 𝐴 ⊆ On
Theorem	onsuci 7791	The successor of an ordinal number is an ordinal number. Inference associated with onsuc 7765 and onsucb 7769. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc 𝐴 ∈ On
Theorem	onuninsuci 7792*	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 7795. (Contributed by NM, 18-Feb-2004.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Theorem	onsucssi 7793	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 7794	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 7795*	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 7792. (Contributed by NM, 18-Feb-2004.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥))
Theorem	ordunisuc2 7796*	An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	ordzsl 7797*	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 7798*	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 7799*	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 7800*	An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))