P. 96 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9501-9600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opwf 9501	An ordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → ⟨𝐴, 𝐵⟩ ∈ ∪ (𝑅1 “ On))
Theorem	unir1 9502	The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of [Mendelson] p. 281. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 8-Jun-2013.)
⊢ ∪ (𝑅1 “ On) = V
Theorem	jech9.3 9503	Every set belongs to some value of the cumulative hierarchy of sets function 𝑅1, i.e. the indexed union of all values of 𝑅1 is the universe. Lemma 9.3 of [Jech] p. 71. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 8-Jun-2013.)
⊢ ∪ 𝑥 ∈ On (𝑅1‘𝑥) = V
Theorem	rankwflem 9504*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 9481 is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Theorem	rankval 9505*	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 9506*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9505 expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
Theorem	rankval2 9507*	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 9508	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 9509	Lemma for rankr1c 9510. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴)))
Theorem	rankr1c 9510	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 9511	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 9512	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 9513	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 9514	A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 9286. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ 𝐴)
Theorem	rankval3b 9515*	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 9516	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 9517	Lemma for rankonid 9518. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝐴 ∈ ∪ (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))
Theorem	rankonid 9518	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 9519	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 9520	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 9521	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 9522	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 9523	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 9524	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 9525	A relationship between rank and 𝑅1, clearly equivalent to ssrankr1 9524 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 9553 for the subset version. (Contributed by Raph Levien, 29-May-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵))
Theorem	r1val2 9526*	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 9527*	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 9528	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 9529*	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 9530*	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 9531*	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 9532	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 9533	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 9534	A stronger property of 𝑅1 than rankpw 9532. 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 9535	Alternate shorter proof of r1pw 9534 based on the additional axioms ax-reg 9281 and ax-inf2 9329. (Contributed by Raph Levien, 29-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵)))
Theorem	r1pwcl 9536	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 9537	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 9538	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 9539	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 9540	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 9541	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 9542*	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 9543	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 9544*	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 9545	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 9546	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 9547	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 9548	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 9549	A set is empty iff its rank is empty. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐴 = ∅ ↔ (rank‘𝐴) = ∅))
Theorem	rankeq0 9550	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 9551	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 9552	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 9553	A relationship between rank and 𝑅1. See rankr1a 9525 for the membership version. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
Theorem	ranksuc 9554	The rank of a successor. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘suc 𝐴) = suc (rank‘𝐴)
Theorem	rankuniss 9555	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 9556*	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 9557*	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 9558*	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 9559*	A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (rank‘𝑥) ∈ (rank‘∪ 𝐴) ↔ (rank‘𝐴) = (rank‘∪ 𝐴))
Theorem	rankc2 9560*	A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘∪ 𝐴) → (rank‘𝐴) = suc (rank‘∪ 𝐴))
Theorem	rankelun 9561	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 9562	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 9563	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 9564	A lower bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
Theorem	rankxpu 9565	An upper bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴 ∪ 𝐵))
Theorem	rankfu 9566	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 9567	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 9568	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 9571 for the successor case. (Contributed by NM, 19-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((Lim (rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵)))
Theorem	rankxplim2 9569	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 9570	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 9571	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 9568 for the limit ordinal case. (Contributed by NM, 19-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (((rank‘(𝐴 ∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = suc suc (rank‘(𝐴 ∪ 𝐵)))
Theorem	tcwf 9572	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 9573	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.9  Scott's trick; collection principle; Hilbert's epsilon
Theorem	scottex 9574*	Scott's trick collects all sets that have a certain property and are of the smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of [Jech] p. 72, is a set. (Contributed by NM, 13-Oct-2003.)
⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V
Theorem	scott0 9575*	Scott's trick collects all sets that have a certain property and are of the smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of [Jech] p. 72, contains at least one representative with the property, if there is one. In other words, the collection is empty iff no set has the property (i.e. 𝐴 is empty). (Contributed by NM, 15-Oct-2003.)
⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅)
Theorem	scottexs 9576*	Theorem scheme version of scottex 9574. The collection of all 𝑥 of minimum rank such that 𝜑(𝑥) is true, is a set. (Contributed by NM, 13-Oct-2003.)
⊢ {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ∈ V
Theorem	scott0s 9577*	Theorem scheme version of scott0 9575. 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.)
⊢ (∃𝑥𝜑 ↔ {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ≠ ∅)
Theorem	cplem1 9578*	Lemma for the Collection Principle cp 9580. (Contributed by NM, 17-Oct-2003.)
⊢ 𝐶 = {𝑦 ∈ 𝐵 ∣ ∀𝑧 ∈ 𝐵 (rank‘𝑦) ⊆ (rank‘𝑧)}    &   ⊢ 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶    ⇒   ⊢ ∀𝑥 ∈ 𝐴 (𝐵 ≠ ∅ → (𝐵 ∩ 𝐷) ≠ ∅)
Theorem	cplem2 9579*	Lemma for the Collection Principle cp 9580. (Contributed by NM, 17-Oct-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥 ∈ 𝐴 (𝐵 ≠ ∅ → (𝐵 ∩ 𝑦) ≠ ∅)
Theorem	cp 9580*	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 scottex 9574 that collapses 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 9581*	A very strong generalization of the Axiom of Replacement (compare zfrep6 7771), derived from the Collection Principle cp 9580. 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 9582*	A variant of the Boundedness Axiom bnd 9581 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 9583*	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.)
⊢ {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ∈ V
Theorem	karden 9584*	If we allow the Axiom of Regularity, we can avoid the Axiom of Choice by defining the cardinal number of a set as the set of all sets equinumerous to it and having the least possible rank. This theorem proves the equinumerosity relationship for this definition (compare carden 10238). The hypotheses correspond to the definition of kard of [Enderton] p. 222 (which we don't define separately since currently we do not use it elsewhere). This theorem along with kardex 9583 justify the definition of kard. The restriction to the least rank prevents the proper class that would result from {𝑥 ∣ 𝑥 ≈ 𝐴}. (Contributed by NM, 18-Dec-2003.) (Revised by AV, 12-Jul-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐶 = {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))}    ⇒   ⊢ (𝐶 = 𝐷 ↔ 𝐴 ≈ 𝐵)
Theorem	htalem 9585*	Lemma for defining an emulation of Hilbert's epsilon. Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/. This theorem is equivalent to Hilbert's "transfinite axiom", described on that page, with the additional 𝑅 We 𝐴 antecedent. The element 𝐵 is the epsilon that the theorem emulates. (Contributed by NM, 11-Mar-2004.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝐴 ≠ ∅) → 𝐵 ∈ 𝐴)
Theorem	hta 9586*	A ZFC emulation of Hilbert's transfinite axiom. The set 𝐵 has the properties of Hilbert's epsilon, except that it also depends on a well-ordering 𝑅. This theorem arose from discussions with Raph Levien on 5-Mar-2004 about translating the HOL proof language, which uses Hilbert's epsilon. See https://us.metamath.org/downloads/choice.txt (copy of obsolete link http://ghilbert.org/choice.txt) and https://us.metamath.org/downloads/megillaward2005he.pdf. Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/. This theorem differs from Hilbert's transfinite axiom described on that page in that it requires 𝑅 We 𝐴 as an antecedent. Class 𝐴 collects the sets of the least rank for which 𝜑(𝑥) is true. Class 𝐵, which emulates Hilbert's epsilon, is the minimum element in a well-ordering 𝑅 on 𝐴. If a well-ordering 𝑅 on 𝐴 can be expressed in a closed form, as might be the case if we are working with say natural numbers, we can eliminate the antecedent with modus ponens, giving us the exact equivalent of Hilbert's transfinite axiom. Otherwise, we replace 𝑅 with a dummy setvar variable, say 𝑤, and attach 𝑤 We 𝐴 as an antecedent in each step of the ZFC version of the HOL proof until the epsilon is eliminated. At that point, 𝐵 (which will have 𝑤 as a free variable) will no longer be present, and we can eliminate 𝑤 We 𝐴 by applying exlimiv 1934 and weth 10182, using scottexs 9576 to establish the existence of 𝐴. For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem 9585. (Contributed by NM, 11-Mar-2004.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐴 = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))}    &   ⊢ 𝐵 = (℩𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ¬ 𝑤𝑅𝑧)    ⇒   ⊢ (𝑅 We 𝐴 → (𝜑 → [𝐵 / 𝑥]𝜑))
2.6.10  Disjoint union
Syntax	cdju 9587	Extend class notation to include disjoint union of two classes.
class (𝐴 ⊔ 𝐵)
Syntax	cinl 9588	Extend class notation to include left injection of a disjoint union.
class inl
Syntax	cinr 9589	Extend class notation to include right injection of a disjoint union.
class inr
Definition	df-dju 9590	Disjoint union of two classes. This is a way of creating a set which contains elements corresponding to each element of 𝐴 or 𝐵, tagging each one with whether it came from 𝐴 or 𝐵. (Contributed by Jim Kingdon, 20-Jun-2022.)
⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
Definition	df-inl 9591	Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.)
⊢ inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩)
Definition	df-inr 9592	Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.)
⊢ inr = (𝑥 ∈ V ↦ ⟨1o, 𝑥⟩)
Theorem	djueq12 9593	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊔ 𝐶) = (𝐵 ⊔ 𝐷))
Theorem	djueq1 9594	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
⊢ (𝐴 = 𝐵 → (𝐴 ⊔ 𝐶) = (𝐵 ⊔ 𝐶))
Theorem	djueq2 9595	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
⊢ (𝐴 = 𝐵 → (𝐶 ⊔ 𝐴) = (𝐶 ⊔ 𝐵))
Theorem	nfdju 9596	Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ⊔ 𝐵)
Theorem	djuex 9597	The disjoint union of sets is a set. For a shorter proof using djuss 9609 see djuexALT 9611. (Contributed by AV, 28-Jun-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ∈ V)
Theorem	djuexb 9598	The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ⊔ 𝐵) ∈ V)
Theorem	djulcl 9599	Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
⊢ (𝐶 ∈ 𝐴 → (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵))
Theorem	djurcl 9600	Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
⊢ (𝐶 ∈ 𝐵 → (inr‘𝐶) ∈ (𝐴 ⊔ 𝐵))