P. 99 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9801-9900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rankwflem 9801*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 9778 is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Theorem	rankval 9802*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). (Contributed by NM, 24-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)}
Theorem	rankvalg 9803*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9802 expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
Theorem	rankval2 9804*	Value of an alternate definition of the rank function. Definition of [BellMachover] p. 478. (Contributed by NM, 8-Oct-2003.)
⊢ (𝐴 ∈ 𝐵 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (𝑅1‘𝑥)})
Theorem	uniwf 9805	A union is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	rankr1clem 9806	Lemma for rankr1c 9807. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴)))
Theorem	rankr1c 9807	A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵))))
Theorem	rankidn 9808	A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ (𝑅1‘(rank‘𝐴)))
Theorem	rankpwi 9809	The rank of a power set. Part of Exercise 30 of [Enderton] p. 207. (Contributed by Mario Carneiro, 3-Jun-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝒫 𝐴) = suc (rank‘𝐴))
Theorem	rankelb 9810	The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) → (𝐴 ∈ 𝐵 → (rank‘𝐴) ∈ (rank‘𝐵)))
Theorem	wfelirr 9811	A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 9576. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ 𝐴)
Theorem	rankval3b 9812*	The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥})
Theorem	ranksnb 9813	The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘{𝐴}) = suc (rank‘𝐴))
Theorem	rankonidlem 9814	Lemma for rankonid 9815. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝐴 ∈ ∪ (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))
Theorem	rankonid 9815	The rank of an ordinal number is itself. Proposition 9.18 of [TakeutiZaring] p. 79 and its converse. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 ↔ (rank‘𝐴) = 𝐴)
Theorem	onwf 9816	The ordinals are all well-founded. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ On ⊆ ∪ (𝑅1 “ On)
Theorem	onssr1 9817	Initial segments of the ordinals are contained in initial segments of the cumulative hierarchy. (Contributed by FL, 20-Apr-2011.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴))
Theorem	rankr1g 9818	A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵))))
Theorem	rankid 9819	Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ (𝑅1‘suc (rank‘𝐴))
Theorem	rankr1 9820	A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by NM, 6-Oct-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵)))
Theorem	ssrankr1 9821	A relationship between an ordinal number less than or equal to a rank, and the cumulative hierarchy of sets 𝑅1. Proposition 9.15(3) of [TakeutiZaring] p. 79. (Contributed by NM, 8-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐵 ⊆ (rank‘𝐴) ↔ ¬ 𝐴 ∈ (𝑅1‘𝐵)))
Theorem	rankr1a 9822	A relationship between rank and 𝑅1, clearly equivalent to ssrankr1 9821 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 9850 for the subset version. (Contributed by Raph Levien, 29-May-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵))
Theorem	r1val2 9823*	The value of the cumulative hierarchy of sets function expressed in terms of rank. Definition 15.19 of [Monk1] p. 113. (Contributed by NM, 30-Nov-2003.)
⊢ (𝐴 ∈ On → (𝑅1‘𝐴) = {𝑥 ∣ (rank‘𝑥) ∈ 𝐴})
Theorem	r1val3 9824*	The value of the cumulative hierarchy of sets function expressed in terms of rank. Theorem 15.18 of [Monk1] p. 113. (Contributed by NM, 30-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ On → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 𝒫 {𝑦 ∣ (rank‘𝑦) ∈ 𝑥})
Theorem	rankel 9825	The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 → (rank‘𝐴) ∈ (rank‘𝐵))
Theorem	rankval3 9826*	The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥}
Theorem	bndrank 9827*	Any class whose elements have bounded rank is a set. Proposition 9.19 of [TakeutiZaring] p. 80. (Contributed by NM, 13-Oct-2003.)
⊢ (∃𝑥 ∈ On ∀𝑦 ∈ 𝐴 (rank‘𝑦) ⊆ 𝑥 → 𝐴 ∈ V)
Theorem	unbndrank 9828*	The elements of a proper class have unbounded rank. Exercise 2 of [TakeutiZaring] p. 80. (Contributed by NM, 13-Oct-2003.)
⊢ (¬ 𝐴 ∈ V → ∀𝑥 ∈ On ∃𝑦 ∈ 𝐴 𝑥 ∈ (rank‘𝑦))
Theorem	rankpw 9829	The rank of a power set. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 22-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘𝒫 𝐴) = suc (rank‘𝐴)
Theorem	ranklim 9830	The rank of a set belongs to a limit ordinal iff the rank of its power set does. (Contributed by NM, 18-Sep-2006.)
⊢ (Lim 𝐵 → ((rank‘𝐴) ∈ 𝐵 ↔ (rank‘𝒫 𝐴) ∈ 𝐵))
Theorem	r1pw 9831	A stronger property of 𝑅1 than rankpw 9829. The latter merely proves that 𝑅1 of the successor is a power set, but here we prove that if 𝐴 is in the cumulative hierarchy, then 𝒫 𝐴 is in the cumulative hierarchy of the successor. (Contributed by Raph Levien, 29-May-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵)))
Theorem	r1pwALT 9832	Alternate shorter proof of r1pw 9831 based on the additional axioms ax-reg 9568 and ax-inf2 9624. (Contributed by Raph Levien, 29-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵)))
Theorem	r1pwcl 9833	The cumulative hierarchy of a limit ordinal is closed under power set. (Contributed by Raph Levien, 29-May-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2014.)
⊢ (Lim 𝐵 → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘𝐵)))
Theorem	rankssb 9834	The subset relation is inherited by the rank function. Exercise 1 of [TakeutiZaring] p. 80. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) → (𝐴 ⊆ 𝐵 → (rank‘𝐴) ⊆ (rank‘𝐵)))
Theorem	rankss 9835	The subset relation is inherited by the rank function. Exercise 1 of [TakeutiZaring] p. 80. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (rank‘𝐴) ⊆ (rank‘𝐵))
Theorem	rankunb 9836	The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵)))
Theorem	rankprb 9837	The rank of an unordered pair. Part of Exercise 30 of [Enderton] p. 207. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘{𝐴, 𝐵}) = suc ((rank‘𝐴) ∪ (rank‘𝐵)))
Theorem	rankopb 9838	The rank of an ordered pair. Part of Exercise 4 of [Kunen] p. 107. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘⟨𝐴, 𝐵⟩) = suc suc ((rank‘𝐴) ∪ (rank‘𝐵)))
Theorem	rankuni2b 9839*	The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥))
Theorem	ranksn 9840	The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112. (Contributed by NM, 28-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘{𝐴}) = suc (rank‘𝐴)
Theorem	rankuni2 9841*	The rank of a union. Part of Theorem 15.17(iv) of [Monk1] p. 112. (Contributed by NM, 30-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥)
Theorem	rankun 9842	The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112. (Contributed by NM, 26-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵))
Theorem	rankpr 9843	The rank of an unordered pair. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 28-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (rank‘{𝐴, 𝐵}) = suc ((rank‘𝐴) ∪ (rank‘𝐵))
Theorem	rankop 9844	The rank of an ordered pair. Part of Exercise 4 of [Kunen] p. 107. (Contributed by NM, 13-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (rank‘⟨𝐴, 𝐵⟩) = suc suc ((rank‘𝐴) ∪ (rank‘𝐵))
Theorem	r1rankid 9845	Any set is a subset of the hierarchy of its rank. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
Theorem	rankeq0b 9846	A set is empty iff its rank is empty. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐴 = ∅ ↔ (rank‘𝐴) = ∅))
Theorem	rankeq0 9847	A set is empty iff its rank is empty. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = ∅ ↔ (rank‘𝐴) = ∅)
Theorem	rankr1id 9848	The rank of the hierarchy of an ordinal number is itself. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 ↔ (rank‘(𝑅1‘𝐴)) = 𝐴)
Theorem	rankuni 9849	The rank of a union. Part of Exercise 4 of [Kunen] p. 107. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (rank‘∪ 𝐴) = ∪ (rank‘𝐴)
Theorem	rankr1b 9850	A relationship between rank and 𝑅1. See rankr1a 9822 for the membership version. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
Theorem	ranksuc 9851	The rank of a successor. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘suc 𝐴) = suc (rank‘𝐴)
Theorem	rankuniss 9852	Upper bound of the rank of a union. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 30-Nov-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘∪ 𝐴) ⊆ (rank‘𝐴)
Theorem	rankval4 9853*	The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of [Jech] p. 72. Also a special case of Theorem 7V(b) of [Enderton] p. 204. (Contributed by NM, 12-Oct-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘𝐴) = ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)
Theorem	rankbnd 9854*	The rank of a set is bounded by a bound for the successor of its members. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝐵 ↔ (rank‘𝐴) ⊆ 𝐵)
Theorem	rankbnd2 9855*	The rank of a set is bounded by the successor of a bound for its members. (Contributed by NM, 15-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (∀𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ 𝐵 ↔ (rank‘𝐴) ⊆ suc 𝐵))
Theorem	rankc1 9856*	A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (rank‘𝑥) ∈ (rank‘∪ 𝐴) ↔ (rank‘𝐴) = (rank‘∪ 𝐴))
Theorem	rankc2 9857*	A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘∪ 𝐴) → (rank‘𝐴) = suc (rank‘∪ 𝐴))
Theorem	rankelun 9858	Rank membership is inherited by union. (Contributed by NM, 18-Sep-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((rank‘𝐴) ∈ (rank‘𝐶) ∧ (rank‘𝐵) ∈ (rank‘𝐷)) → (rank‘(𝐴 ∪ 𝐵)) ∈ (rank‘(𝐶 ∪ 𝐷)))
Theorem	rankelpr 9859	Rank membership is inherited by unordered pairs. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((rank‘𝐴) ∈ (rank‘𝐶) ∧ (rank‘𝐵) ∈ (rank‘𝐷)) → (rank‘{𝐴, 𝐵}) ∈ (rank‘{𝐶, 𝐷}))
Theorem	rankelop 9860	Rank membership is inherited by ordered pairs. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((rank‘𝐴) ∈ (rank‘𝐶) ∧ (rank‘𝐵) ∈ (rank‘𝐷)) → (rank‘⟨𝐴, 𝐵⟩) ∈ (rank‘⟨𝐶, 𝐷⟩))
Theorem	rankxpl 9861	A lower bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
Theorem	rankxpu 9862	An upper bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴 ∪ 𝐵))
Theorem	rankfu 9863	An upper bound on the rank of a function. (Contributed by Gérard Lang, 5-Aug-2018.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴⟶𝐵 → (rank‘𝐹) ⊆ suc suc (rank‘(𝐴 ∪ 𝐵)))
Theorem	rankmapu 9864	An upper bound on the rank of set exponentiation. (Contributed by Gérard Lang, 5-Aug-2018.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (rank‘(𝐴 ↑m 𝐵)) ⊆ suc suc suc (rank‘(𝐴 ∪ 𝐵))
Theorem	rankxplim 9865	The rank of a Cartesian product when the rank of the union of its arguments is a limit ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxpsuc 9868 for the successor case. (Contributed by NM, 19-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((Lim (rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵)))
Theorem	rankxplim2 9866	If the rank of a Cartesian product is a limit ordinal, so is the rank of the union of its arguments. (Contributed by NM, 19-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 ∪ 𝐵)))
Theorem	rankxplim3 9867	The rank of a Cartesian product is a limit ordinal iff its union is. (Contributed by NM, 19-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim ∪ (rank‘(𝐴 × 𝐵)))
Theorem	rankxpsuc 9868	The rank of a Cartesian product when the rank of the union of its arguments is a successor ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxplim 9865 for the limit ordinal case. (Contributed by NM, 19-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (((rank‘(𝐴 ∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = suc suc (rank‘(𝐴 ∪ 𝐵)))
Theorem	tcwf 9869	The transitive closure function is well-founded if its argument is. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) ∈ ∪ (𝑅1 “ On))
Theorem	tcrank 9870	This theorem expresses two different facts from the two subset implications in this equality. In the forward direction, it says that the transitive closure has members of every rank below 𝐴. Stated another way, to construct a set at a given rank, you have to climb the entire hierarchy of ordinals below (rank‘𝐴), constructing at least one set at each level in order to move up the ranks. In the reverse direction, it says that every member of (TC‘𝐴) has a rank below the rank of 𝐴, since intuitively it contains only the members of 𝐴 and the members of those and so on, but nothing "bigger" than 𝐴. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))
2.6.10  Scott's trick; collection principle; Hilbert's epsilon
Syntax	cscott 9871	Extend class notation with the Scott's trick operation.
class Scott 𝐴
Definition	df-scott 9872*	Define an operation for Scott's trick, expressed as in Equation 9.3 of [Jech] p. 72. Scott's trick collects all sets that have a certain property and are of the smallest possible rank. The resulting collection is guaranteed to be a set (see scottex 9876). Under this definition, the property in question is represented by membership in a class. See scottab 9883 for the case where a wff (meta)variable is used to represent the property. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ Scott 𝐴 = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}
Theorem	scotteqd 9873	Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵)
Theorem	scotteq 9874	Closed form of scotteqd 9873. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵)
Theorem	nfscott 9875	Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Scott 𝐴
Theorem	scottex 9876	Scott's trick produces a set. (Contributed by NM, 13-Oct-2003.) Use the Scott operation. (Revised by BTernaryTau, 18-Jul-2026.)
⊢ Scott 𝐴 ∈ V
Theorem	scottexOLD 9877*	Obsolete version of scottex 9876 as of 18-Jul-2026. (Contributed by NM, 13-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V
Theorem	scottss 9878	Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Scott 𝐴 ⊆ 𝐴
Theorem	scott0 9879	Applying Scott's trick to the empty set leaves it unchanged. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ Scott ∅ = ∅
Theorem	scott0b 9880	Applying Scott's trick yields the empty set iff it was applied to the empty set. (Contributed by NM, 15-Oct-2003.) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026.)
⊢ (𝐴 = ∅ ↔ Scott 𝐴 = ∅)
Theorem	scott0OLD 9881*	Obsolete version of scott0b 9880 as of 19-Jul-2026. (Contributed by NM, 15-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅)
Theorem	scottabf 9882*	Value of the Scott operation at a class abstraction. Variant of scottab 9883 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottab 9883*	Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottabes 9884*	Value of the Scott operation at a class abstraction. Variant of scottab 9883 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	elscottab 9885*	An element of the output of the Scott operation applied to a class abstraction satisfies the class abstraction's predicate. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑦 ∈ Scott {𝑥 ∣ 𝜑} → 𝜓)
Theorem	scottexsOLD 9886*	Obsolete theorem as of 27-Jul-2026. Use scottex 9876 with a class abstraction instead. (Contributed by NM, 13-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ∈ V
Theorem	scott0bs 9887	Theorem scheme version of scott0b 9880. The collection of all 𝑥 of minimum rank such that 𝜑(𝑥) is true, is not empty iff there is an 𝑥 such that 𝜑(𝑥) holds. (Contributed by NM, 13-Oct-2003.) Use the Scott operation. (Revised by BTernaryTau, 22-Jul-2026.)
⊢ (∃𝑥𝜑 ↔ Scott {𝑥 ∣ 𝜑} ≠ ∅)
Theorem	scott0bsOLD 9888*	Obsolete version of scott0bs 9887 as of 19-Jul-2026. (Contributed by NM, 13-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 ↔ {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ≠ ∅)
Theorem	scottex2OLD 9889	Obsolete version of scottex 9876 as of 18-Jul-2026. (Contributed by Rohan Ridenour, 9-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Scott 𝐴 ∈ V
Theorem	scotteld 9890*	The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴)
Theorem	scottelrankd 9891	Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶))
Theorem	scottrankd 9892	Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵))
Theorem	cplem1 9893	Lemma for the Collection Principle cp 9897. (Contributed by NM, 17-Oct-2003.) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026.)
⊢ 𝐶 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵    ⇒   ⊢ ∀𝑥 ∈ 𝐴 (𝐵 ≠ ∅ → (𝐵 ∩ 𝐶) ≠ ∅)
Theorem	cplem1OLD 9894*	Obsolete version of cplem1 9893 as of 19-Jul-2026. (Contributed by NM, 17-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐶 = {𝑦 ∈ 𝐵 ∣ ∀𝑧 ∈ 𝐵 (rank‘𝑦) ⊆ (rank‘𝑧)}    &   ⊢ 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶    ⇒   ⊢ ∀𝑥 ∈ 𝐴 (𝐵 ≠ ∅ → (𝐵 ∩ 𝐷) ≠ ∅)
Theorem	cplem2 9895*	Lemma for the Collection Principle cp 9897. (Contributed by NM, 17-Oct-2003.) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥 ∈ 𝐴 (𝐵 ≠ ∅ → (𝐵 ∩ 𝑦) ≠ ∅)
Theorem	cplem2OLD 9896*	Obsolete version of cplem2 9895 as of 19-Jul-2026. (Contributed by NM, 17-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥 ∈ 𝐴 (𝐵 ≠ ∅ → (𝐵 ∩ 𝑦) ≠ ∅)
Theorem	cp 9897*	Collection Principle. This remarkable theorem scheme is in effect a very strong generalization of the Axiom of Replacement. The proof makes use of Scott's trick df-scott 9872 to collapse a proper class into a set of minimum rank. The wff 𝜑 can be thought of as 𝜑(𝑥, 𝑦). Scheme "Collection Principle" of [Jech] p. 72. (Contributed by NM, 17-Oct-2003.)
⊢ ∃𝑤∀𝑥 ∈ 𝑧 (∃𝑦𝜑 → ∃𝑦 ∈ 𝑤 𝜑)
Theorem	bnd 9898*	A very strong generalization of the Axiom of Replacement (compare zfrep6 5248), derived from the Collection Principle cp 9897. Its strength lies in the rather profound fact that 𝜑(𝑥, 𝑦) does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. (Contributed by NM, 17-Oct-2004.)
⊢ (∀𝑥 ∈ 𝑧 ∃𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
Theorem	bnd2 9899*	A variant of the Boundedness Axiom bnd 9898 that picks a subset 𝑧 out of a possibly proper class 𝐵 in which a property is true. (Contributed by NM, 4-Feb-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑))
Theorem	kardex 9900	The collection of all sets equinumerous to a set 𝐴 and having the least possible rank is a set. This is the part of the justification of the definition of kard of [Enderton] p. 222. (Contributed by NM, 14-Dec-2003.) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026.)
⊢ Scott {𝑥 ∣ 𝑥 ≈ 𝐴} ∈ V