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
2.3.22  Proper subset relation
Syntax	crpss 7701	Extend class notation to include the reified proper subset relation.
class [⊊]
Definition	df-rpss 7702*	Define a relation which corresponds to proper subsethood df-pss 3937 on sets. This allows to use proper subsethood with general concepts that require relations, such as strict ordering, see sorpss 7707. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ [⊊] = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}
Theorem	relrpss 7703	The proper subset relation is a relation. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ Rel [⊊]
Theorem	brrpssg 7704	The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	brrpss 7705	The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵)
Theorem	porpss 7706	Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ [⊊] Po 𝐴
Theorem	sorpss 7707*	Express strict ordering under proper subsets, i.e. the notion of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ( [⊊] Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
Theorem	sorpssi 7708	Property of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵))
Theorem	sorpssun 7709	A chain of sets is closed under binary union. (Contributed by Mario Carneiro, 16-May-2015.)
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∪ 𝐶) ∈ 𝐴)
Theorem	sorpssin 7710	A chain of sets is closed under binary intersection. (Contributed by Mario Carneiro, 16-May-2015.)
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∩ 𝐶) ∈ 𝐴)
Theorem	sorpssuni 7711*	In a chain of sets, a maximal element is the union of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ( [⊊] Or 𝑌 → (∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 ↔ ∪ 𝑌 ∈ 𝑌))
Theorem	sorpssint 7712*	In a chain of sets, a minimal element is the intersection of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ( [⊊] Or 𝑌 → (∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∩ 𝑌 ∈ 𝑌))
Theorem	sorpsscmpl 7713*	The componentwise complement of a chain of sets is also a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ( [⊊] Or 𝑌 → [⊊] Or {𝑢 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑢) ∈ 𝑌})
2.4  ZF Set Theory - add the Axiom of Union
2.4.1  Introduce the Axiom of Union
Axiom	ax-un 7714*	Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states that a set 𝑦 exists that includes the union of a given set 𝑥 i.e. the collection of all members of the members of 𝑥. The variant axun2 7716 states that the union itself exists. A version with the standard abbreviation for union is uniex2 7717. A version using class notation is uniex 7720. The union of a class df-uni 4875 should not be confused with the union of two classes df-un 3922. Their relationship is shown in unipr 4891. (Contributed by NM, 23-Dec-1993.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfun 7715*	Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) Use ax-un 7714 instead. (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axun2 7716*	A variant of the Axiom of Union ax-un 7714. For any set 𝑥, there exists a set 𝑦 whose members are exactly the members of the members of 𝑥 i.e. the union of 𝑥. Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
Theorem	uniex2 7717*	The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦 𝑦 = ∪ 𝑥
Theorem	vuniex 7718	The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) (Revised by BJ, 6-Apr-2024.)
⊢ ∪ 𝑥 ∈ V
Theorem	uniexg 7719	The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.)
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
Theorem	uniex 7720	The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3464), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ 𝐴 ∈ V
Theorem	uniexd 7721	Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ V)
Theorem	unexg 7722	The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) Prove unexg 7722 first and then unex 7723 and unexb 7726 from it. (Revised by BJ, 21-Jul-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	unex 7723	The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ V
Theorem	unexOLD 7724	Obsolete version of unex 7723 as of 21-Jul-2025. (Contributed by NM, 1-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ V
Theorem	tpex 7725	An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)
⊢ {𝐴, 𝐵, 𝐶} ∈ V
Theorem	unexb 7726	Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
Theorem	unexbOLD 7727	Obsolete version of unexb 7726 as of 21-Jul-2025. (Contributed by NM, 11-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
Theorem	unexgOLD 7728	Obsolete version of unexg 7722 as of 21-Jul-2025. (Contributed by NM, 18-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	xpexg 7729	The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7963. (Contributed by NM, 14-Aug-1994.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
Theorem	xpexd 7730	The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)
Theorem	3xpexg 7731	The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
⊢ (𝑉 ∈ 𝑊 → ((𝑉 × 𝑉) × 𝑉) ∈ V)
Theorem	xpex 7732	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 7733	The union of two sets is a set. (Contributed by SN, 16-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)
Theorem	sqxpexg 7734	The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)
Theorem	abnexg 7735*	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 7942. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 7737 and pwnex 7738 respectively, proved from abnex 7736, which is a consequence of abnexg 7735 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.)
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V))
Theorem	abnex 7736*	Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 7737 and pwnex 7738. See the comment of abnexg 7735. (Contributed by BJ, 2-May-2021.)
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V)
Theorem	snnex 7737*	The class of all singletons is a proper class. See also pwnex 7738. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof shortened by BJ, 5-Dec-2021.)
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V
Theorem	pwnex 7738*	The class of all power sets is a proper class. See also snnex 7737. (Contributed by BJ, 2-May-2021.)
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V
Theorem	difex2 7739	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 7740	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 7741*	Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007.)
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)}
Theorem	uniexr 7742	Converse of the Axiom of Union. Note that it does not require ax-un 7714. (Contributed by NM, 11-Nov-2003.)
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V)
Theorem	uniexb 7743	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 7744	Converse of the Axiom of Power Sets. Note that it does not require ax-pow 5323. (Contributed by NM, 11-Nov-2003.)
⊢ (𝒫 𝐴 ∈ 𝑉 → 𝐴 ∈ V)
Theorem	pwexb 7745	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 7746	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 7747	Membership in a power class difference. (Contributed by NM, 25-Mar-2007.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵))
Theorem	elpwun 7748	Membership in the power class of a union. (Contributed by NM, 26-Mar-2007.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝒫 (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐶) ∈ 𝒫 𝐵)
Theorem	pwuncl 7749	Power classes are closed under union. (Contributed by AV, 27-Feb-2024.)
⊢ ((𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋) → (𝐴 ∪ 𝐵) ∈ 𝒫 𝑋)
Theorem	iunpw 7750*	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 7751	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 7752	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 7753*	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 7754	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 7714, see epweonALT 7755. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7714. (Revised by BTernaryTau, 30-Nov-2024.)
⊢ E We On
Theorem	epweonALT 7755	Alternate proof of epweon 7754, shorter but requiring ax-un 7714. (Contributed by NM, 1-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ E We On
Theorem	ordon 7756	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 7757	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 7756), 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 7758	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 7759	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 7760	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 7761	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 7762	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 7763	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 7764	An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
Theorem	predon 7765	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 7766	Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ⊆ On → (𝐴 ∉ V ↔ ∪ 𝐴 = On))
Theorem	onuni 7767	The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On)
Theorem	orduni 7768	The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.)
⊢ (Ord 𝐴 → Ord ∪ 𝐴)
Theorem	onint 7769	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 7770	The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ⊆ On → (∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴))
Theorem	onssmin 7771*	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 7772	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 7773	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 7774	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 7775	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 7776	An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003.)
⊢ (∃𝑥 ∈ On 𝜑 ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On)
Theorem	onnmin 7777	No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997.)
⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵 ∈ ∩ 𝐴)
Theorem	onnminsb 7778*	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 7779*	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 7780*	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 7781*	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 7782	The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003.)
⊢ suc On = On
Theorem	sucexb 7783	A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.)
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
Theorem	sucexg 7784	The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V)
Theorem	sucex 7785	The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ suc 𝐴 ∈ V
Theorem	onmindif2 7786	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 7787	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 7790. (Revised by BTernaryTau, 6-Jan-2025.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ (Ord 𝐴 → Ord suc 𝐴)
Theorem	sucexeloni 7788	If the successor of an ordinal number exists, it is an ordinal number. This variation of onsuc 7790 does not require ax-un 7714. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉) → suc 𝐴 ∈ On)
Theorem	sucexeloniOLD 7789	Obsolete version of sucexeloni 7788 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 7790	The successor of an ordinal number is an ordinal number. Closed form of onsuci 7817. Forward implication of onsucb 7795. 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 7791	A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7714. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
Theorem	ordsucOLD 7792	Obsolete version of ordsuc 7791 as of 6-Jan-2025. (Contributed by NM, 3-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
Theorem	ordpwsuc 7793	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 7794	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 7795	A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc 7790. (Contributed by NM, 9-Sep-2003.)
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)
Theorem	ordsucss 7796	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 7797	An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ On → 𝐴 ⊊ suc 𝐴)
Theorem	ordelsuc 7798	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 7799*	The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.)
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥})
Theorem	ordsucelsuc 7800	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 𝐵))