P. 93 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9201-9300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tz9.12lem2 9201*	Lemma for tz9.12 9203. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ suc ∪ (𝐹 “ 𝐴) ∈ On
Theorem	tz9.12lem3 9202*	Lemma for tz9.12 9203. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → 𝐴 ∈ (𝑅1‘suc suc ∪ (𝐹 “ 𝐴)))
Theorem	tz9.12 9203*	A set is well-founded if all of its elements are well-founded. Proposition 9.12 of [TakeutiZaring] p. 78. The main proof consists of tz9.12lem1 9200 through tz9.12lem3 9202. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘𝑦))
Theorem	tz9.13 9204*	Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of [TakeutiZaring] p. 78. (Contributed by NM, 23-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥)
Theorem	tz9.13g 9205*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 9204 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥))
Theorem	rankwflemb 9206*	Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Theorem	rankf 9207	The domain and range of the rank function. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 12-Sep-2013.)
⊢ rank:∪ (𝑅1 “ On)⟶On
Theorem	rankon 9208	The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 12-Sep-2013.)
⊢ (rank‘𝐴) ∈ On
Theorem	r1elwf 9209	Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	rankvalb 9210*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9229 does not use Regularity, and so requires the assumption that 𝐴 is in the range of 𝑅1. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
Theorem	rankr1ai 9211	One direction of rankr1a 9249. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → (rank‘𝐴) ∈ 𝐵)
Theorem	rankvaln 9212	Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 9226, unless 𝐴 is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (¬ 𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∅)
Theorem	rankidb 9213	Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ∈ (𝑅1‘suc (rank‘𝐴)))
Theorem	rankdmr1 9214	A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (rank‘𝐴) ∈ dom 𝑅1
Theorem	rankr1ag 9215	A version of rankr1a 9249 that is suitable without assuming Regularity or Replacement. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵))
Theorem	rankr1bg 9216	A relationship between rank and 𝑅1. See rankr1ag 9215 for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
Theorem	r1rankidb 9217	Any set is a subset of the hierarchy of its rank. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
Theorem	r1elssi 9218	The range of the 𝑅1 function is transitive. Lemma 2.10 of [Kunen] p. 97. One direction of r1elss 9219 that doesn't need 𝐴 to be a set. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On))
Theorem	r1elss 9219	The range of the 𝑅1 function is transitive. Lemma 2.10 of [Kunen] p. 97. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝐴 ⊆ ∪ (𝑅1 “ On))
Theorem	pwwf 9220	A power set is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝒫 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	sswf 9221	A subset of a well-founded set is well-founded. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ ∪ (𝑅1 “ On))
Theorem	snwf 9222	A singleton is well-founded if its element is. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝐴} ∈ ∪ (𝑅1 “ On))
Theorem	unwf 9223	A binary union is well-founded iff its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) ↔ (𝐴 ∪ 𝐵) ∈ ∪ (𝑅1 “ On))
Theorem	prwf 9224	An unordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → {𝐴, 𝐵} ∈ ∪ (𝑅1 “ On))
Theorem	opwf 9225	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 9226	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 9227	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 9228*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 9205 is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Theorem	rankval 9229*	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 9230*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9229 expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
Theorem	rankval2 9231*	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 9232	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 9233	Lemma for rankr1c 9234. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴)))
Theorem	rankr1c 9234	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 9235	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 9236	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 9237	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 9238	A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 9045. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ 𝐴)
Theorem	rankval3b 9239*	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 9240	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 9241	Lemma for rankonid 9242. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝐴 ∈ ∪ (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))
Theorem	rankonid 9242	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 9243	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 9244	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 9245	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 9246	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 9247	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 9248	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 9249	A relationship between rank and 𝑅1, clearly equivalent to ssrankr1 9248 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 9277 for the subset version. (Contributed by Raph Levien, 29-May-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵))
Theorem	r1val2 9250*	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 9251*	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 9252	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 9253*	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 9254*	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 9255*	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 9256	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 9257	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 9258	A stronger property of 𝑅1 than rankpw 9256. 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 9259	Alternate shorter proof of r1pw 9258 based on the additional axioms ax-reg 9040 and ax-inf2 9088. (Contributed by Raph Levien, 29-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵)))
Theorem	r1pwcl 9260	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 9261	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 9262	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 9263	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 9264	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 9265	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 9266*	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 9267	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 9268*	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 9269	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 9270	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 9271	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 9272	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 9273	A set is empty iff its rank is empty. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐴 = ∅ ↔ (rank‘𝐴) = ∅))
Theorem	rankeq0 9274	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 9275	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 9276	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 9277	A relationship between rank and 𝑅1. See rankr1a 9249 for the membership version. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
Theorem	ranksuc 9278	The rank of a successor. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘suc 𝐴) = suc (rank‘𝐴)
Theorem	rankuniss 9279	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 9280*	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 9281*	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 9282*	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 9283*	A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (rank‘𝑥) ∈ (rank‘∪ 𝐴) ↔ (rank‘𝐴) = (rank‘∪ 𝐴))
Theorem	rankc2 9284*	A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘∪ 𝐴) → (rank‘𝐴) = suc (rank‘∪ 𝐴))
Theorem	rankelun 9285	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 9286	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 9287	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 9288	A lower bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
Theorem	rankxpu 9289	An upper bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴 ∪ 𝐵))
Theorem	rankfu 9290	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 9291	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 9292	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 9295 for the successor case. (Contributed by NM, 19-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((Lim (rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵)))
Theorem	rankxplim2 9293	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 9294	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 9295	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 9292 for the limit ordinal case. (Contributed by NM, 19-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (((rank‘(𝐴 ∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = suc suc (rank‘(𝐴 ∪ 𝐵)))
Theorem	tcwf 9296	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 9297	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.6  Scott's trick; collection principle; Hilbert's epsilon
Theorem	scottex 9298*	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 9299*	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 9300*	Theorem scheme version of scottex 9298. The collection of all 𝑥 of minimum rank such that 𝜑(𝑥) is true, is a set. (Contributed by NM, 13-Oct-2003.)
⊢ {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ∈ V