P. 98 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	r1tr2 9701	The union of a cumulative hierarchy of sets at ordinal 𝐴 is a subset of the hierarchy at 𝐴. JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011.)
⊢ ∪ (𝑅1‘𝐴) ⊆ (𝑅1‘𝐴)
Theorem	r1ordg 9702	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.)
⊢ (𝐵 ∈ dom 𝑅1 → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ∈ (𝑅1‘𝐵)))
Theorem	r1ord3g 9703	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.)
⊢ ((𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1ord 9704	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ∈ (𝑅1‘𝐵)))
Theorem	r1ord2 9705	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 22-Sep-2003.)
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1ord3 9706	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1sssuc 9707	The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011.)
⊢ (𝐴 ∈ On → (𝑅1‘𝐴) ⊆ (𝑅1‘suc 𝐴))
Theorem	r1pwss 9708	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
Theorem	r1sscl 9709	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐶 ⊆ 𝐴) → 𝐶 ∈ (𝑅1‘𝐵))
Theorem	r1val1 9710*	The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 𝒫 (𝑅1‘𝑥))
Theorem	tz9.12lem1 9711*	Lemma for tz9.12 9714. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ (𝐹 “ 𝐴) ⊆ On
Theorem	tz9.12lem2 9712*	Lemma for tz9.12 9714. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ suc ∪ (𝐹 “ 𝐴) ∈ On
Theorem	tz9.12lem3 9713*	Lemma for tz9.12 9714. (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 9714*	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 9711 through tz9.12lem3 9713. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘𝑦))
Theorem	tz9.13 9715*	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 9716*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 9715 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥))
Theorem	rankwflemb 9717*	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 9718	The domain and codomain of the rank function. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 12-Sep-2013.)
⊢ rank:∪ (𝑅1 “ On)⟶On
Theorem	rankon 9719	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 9720	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 9721*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9740 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 9722	One direction of rankr1a 9760. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → (rank‘𝐴) ∈ 𝐵)
Theorem	rankvaln 9723	Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 9737, unless 𝐴 is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (¬ 𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∅)
Theorem	rankidb 9724	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 9725	A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (rank‘𝐴) ∈ dom 𝑅1
Theorem	rankr1ag 9726	A version of rankr1a 9760 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 9727	A relationship between rank and 𝑅1. See rankr1ag 9726 for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
Theorem	r1rankidb 9728	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 9729	The range of the 𝑅1 function is transitive. Lemma 2.10 of [Kunen] p. 97. One direction of r1elss 9730 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 9730	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 9731	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 9732	A subset of a well-founded set is well-founded. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ ∪ (𝑅1 “ On))
Theorem	snwf 9733	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 9734	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 9735	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 9736	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 9737	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 9738	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 9739*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 9716 is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Theorem	rankval 9740*	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 9741*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9740 expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
Theorem	rankval2 9742*	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 9743	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 9744	Lemma for rankr1c 9745. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴)))
Theorem	rankr1c 9745	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 9746	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 9747	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 9748	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 9749	A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 9516. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ 𝐴)
Theorem	rankval3b 9750*	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 9751	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 9752	Lemma for rankonid 9753. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝐴 ∈ ∪ (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))
Theorem	rankonid 9753	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 9754	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 9755	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 9756	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 9757	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 9758	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 9759	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 9760	A relationship between rank and 𝑅1, clearly equivalent to ssrankr1 9759 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 9788 for the subset version. (Contributed by Raph Levien, 29-May-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵))
Theorem	r1val2 9761*	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 9762*	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 9763	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 9764*	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 9765*	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 9766*	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 9767	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 9768	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 9769	A stronger property of 𝑅1 than rankpw 9767. 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 9770	Alternate shorter proof of r1pw 9769 based on the additional axioms ax-reg 9509 and ax-inf2 9562. (Contributed by Raph Levien, 29-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵)))
Theorem	r1pwcl 9771	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 9772	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 9773	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 9774	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 9775	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 9776	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 9777*	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 9778	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 9779*	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 9780	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 9781	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 9782	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 9783	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 9784	A set is empty iff its rank is empty. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐴 = ∅ ↔ (rank‘𝐴) = ∅))
Theorem	rankeq0 9785	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 9786	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 9787	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 9788	A relationship between rank and 𝑅1. See rankr1a 9760 for the membership version. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
Theorem	ranksuc 9789	The rank of a successor. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rank‘suc 𝐴) = suc (rank‘𝐴)
Theorem	rankuniss 9790	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 9791*	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 9792*	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 9793*	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 9794*	A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (rank‘𝑥) ∈ (rank‘∪ 𝐴) ↔ (rank‘𝐴) = (rank‘∪ 𝐴))
Theorem	rankc2 9795*	A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘∪ 𝐴) → (rank‘𝐴) = suc (rank‘∪ 𝐴))
Theorem	rankelun 9796	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 9797	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 9798	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 9799	A lower bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
Theorem	rankxpu 9800	An upper bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴 ∪ 𝐵))