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	unexd 7701	The union of two sets is a set. (Contributed by SN, 16-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)
Theorem	sqxpexg 7702	The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)
Theorem	abnexg 7703*	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 7907. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 7705 and pwnex 7706 respectively, proved from abnex 7704, which is a consequence of abnexg 7703 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.)
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V))
Theorem	abnex 7704*	Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 7705 and pwnex 7706. See the comment of abnexg 7703. (Contributed by BJ, 2-May-2021.)
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V)
Theorem	snnex 7705*	The class of all singletons is a proper class. See also pwnex 7706. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof shortened by BJ, 5-Dec-2021.)
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V
Theorem	pwnex 7706*	The class of all power sets is a proper class. See also snnex 7705. (Contributed by BJ, 2-May-2021.)
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V
Theorem	difex2 7707	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 7708	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 7709*	Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007.)
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)}
Theorem	uniexr 7710	Converse of the Axiom of Union. Note that it does not require ax-un 7682. (Contributed by NM, 11-Nov-2003.)
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V)
Theorem	uniexb 7711	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 7712	Converse of the Axiom of Power Sets. Note that it does not require ax-pow 5302. (Contributed by NM, 11-Nov-2003.)
⊢ (𝒫 𝐴 ∈ 𝑉 → 𝐴 ∈ V)
Theorem	pwexb 7713	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 7714	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 7715	Membership in a power class difference. (Contributed by NM, 25-Mar-2007.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵))
Theorem	elpwun 7716	Membership in the power class of a union. (Contributed by NM, 26-Mar-2007.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝒫 (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐶) ∈ 𝒫 𝐵)
Theorem	pwuncl 7717	Power classes are closed under union. (Contributed by AV, 27-Feb-2024.)
⊢ ((𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋) → (𝐴 ∪ 𝐵) ∈ 𝒫 𝑋)
Theorem	iunpw 7718*	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 7719	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 7720	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 7721*	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 7722	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 7682, see epweonALT 7723. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7682. (Revised by BTernaryTau, 30-Nov-2024.)
⊢ E We On
Theorem	epweonALT 7723	Alternate proof of epweon 7722, shorter but requiring ax-un 7682. (Contributed by NM, 1-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ E We On
Theorem	ordon 7724	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 7725	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 7724), 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 7726	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 7727	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 7728	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 7729	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 7730	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 7731	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 7732	An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
Theorem	predon 7733	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 7734	Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ⊆ On → (𝐴 ∉ V ↔ ∪ 𝐴 = On))
Theorem	onuni 7735	The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On)
Theorem	orduni 7736	The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.)
⊢ (Ord 𝐴 → Ord ∪ 𝐴)
Theorem	onint 7737	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 7738	The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ⊆ On → (∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴))
Theorem	onssmin 7739*	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 7740	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 7741	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 7742	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 7743	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 7744	An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003.)
⊢ (∃𝑥 ∈ On 𝜑 ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On)
Theorem	onnmin 7745	No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997.)
⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵 ∈ ∩ 𝐴)
Theorem	onnminsb 7746*	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 7747*	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 7748*	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 7749*	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 7750	The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003.)
⊢ suc On = On
Theorem	sucexb 7751	A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.)
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
Theorem	sucexg 7752	The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V)
Theorem	sucex 7753	The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ suc 𝐴 ∈ V
Theorem	onmindif2 7754	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 7755	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 7757. (Revised by BTernaryTau, 6-Jan-2025.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ (Ord 𝐴 → Ord suc 𝐴)
Theorem	sucexeloni 7756	If the successor of an ordinal number exists, it is an ordinal number. This variation of onsuc 7757 does not require ax-un 7682. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉) → suc 𝐴 ∈ On)
Theorem	onsuc 7757	The successor of an ordinal number is an ordinal number. Closed form of onsuci 7783. Forward implication of onsucb 7761. 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 7758	A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7682. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
Theorem	ordpwsuc 7759	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 7760	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 7761	A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc 7757. (Contributed by NM, 9-Sep-2003.)
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)
Theorem	ordsucss 7762	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 7763	An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ On → 𝐴 ⊊ suc 𝐴)
Theorem	ordelsuc 7764	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 7765*	The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.)
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥})
Theorem	ordsucelsuc 7766	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 7767	The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵))
Theorem	ordsucuniel 7768	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 7769	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 7770	The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∪ 𝐶) ∈ {𝐵, 𝐶})
Theorem	ordunel 7771	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 7772	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 7773	An ordinal class is a subclass of the successor of its union. (Contributed by NM, 12-Sep-2003.)
⊢ (Ord 𝐴 → 𝐴 ⊆ suc ∪ 𝐴)
Theorem	orduniorsuc 7774	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 7775	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 7776	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 7777*	The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005.)
⊢ (Ord 𝐴 → ∪ {𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴} = 𝐴)
Theorem	onsucuni2 7778	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 7779	The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995.)
⊢ (Ord 𝐴 → ∅ ∈ suc 𝐴)
Theorem	limon 7780	The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.)
⊢ Lim On
Theorem	onuniorsuc 7781	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 7782	An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ 𝐴 ⊆ On
Theorem	onsuci 7783	The successor of an ordinal number is an ordinal number. Inference associated with onsuc 7757 and onsucb 7761. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc 𝐴 ∈ On
Theorem	onuninsuci 7784*	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 7787. (Contributed by NM, 18-Feb-2004.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Theorem	onsucssi 7785	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 7786	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 7787*	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 7784. (Contributed by NM, 18-Feb-2004.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥))
Theorem	ordunisuc2 7788*	An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	ordzsl 7789*	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 7790*	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 7791*	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 7792*	An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	limsuc 7793	The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.)
⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))
Theorem	limsssuc 7794	A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003.)
⊢ (Lim 𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵))
Theorem	nlimon 7795*	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 7796*	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 7797*	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 7807 or tfinds 7804 for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004.)
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → 𝐴 = On)
Theorem	tfisg 7798*	A closed form of tfis 7799. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑)
Theorem	tfis 7799*	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 7800*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝑥 ∈ On → 𝜑)