P. 90 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tc0 8901	The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015.)
⊢ (TC‘∅) = ∅
Theorem	tc00 8902	The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.)
⊢ (𝐴 ∈ 𝑉 → ((TC‘𝐴) = ∅ ↔ 𝐴 = ∅))
2.6.5  Rank
Syntax	cr1 8903	Extend class definition to include the cumulative hierarchy of sets function.
class 𝑅1
Syntax	crnk 8904	Extend class definition to include rank function.
class rank
Definition	df-r1 8905	Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation (𝑅1). Starting with the empty set, this function builds up layers of sets where the next layer is the power set of the previous layer (and the union of previous layers when the argument is a limit ordinal). Using the Axiom of Regularity, we can show that any set whatsoever belongs to one of the layers of this hierarchy (see tz9.13 8932). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 8909, r1suc 8911, and r1lim 8913. Theorem r1val1 8927 shows a recursive definition that works for all values, and theorems r1val2 8978 and r1val3 8979 show the value expressed in terms of rank. Other notations for this function are R with the argument as a subscript (Equation 3.1 of [BellMachover] p. 477), V with a subscript (Definition of [Enderton] p. 202), M with a subscript (Definition 15.19 of [Monk1] p. 113), the capital Greek letter psi (Definition of [Mendelson] p. 281), and bold-face R (Definition 2.1 of [Kunen] p. 95). (Contributed by NM, 2-Sep-2003.)
⊢ 𝑅1 = rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅)
Definition	df-rank 8906*	Define the rank function. See rankval 8957, rankval2 8959, rankval3 8981, or rankval4 9008 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function 𝑅1: given a set, it returns an ordinal number telling us the smallest layer of the hierarchy to which the set belongs. Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem rankid 8974 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 8977. (Contributed by NM, 11-Oct-2003.)
⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
Theorem	r1funlim 8907	The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon 8908 avoids ax-rep 4995.) (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
Theorem	r1fnon 8908	The cumulative hierarchy of sets function is a function on the class of ordinal numbers. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ 𝑅1 Fn On
Theorem	r10 8909	Value of the cumulative hierarchy of sets function at ∅. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝑅1‘∅) = ∅
Theorem	r1sucg 8910	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1‘𝐴))
Theorem	r1suc 8911	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝐴 ∈ On → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1‘𝐴))
Theorem	r1limg 8912*	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
Theorem	r1lim 8913*	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
Theorem	r1fin 8914	The first ω levels of the cumulative hierarchy are all finite. (Contributed by Mario Carneiro, 15-May-2013.)
⊢ (𝐴 ∈ ω → (𝑅1‘𝐴) ∈ Fin)
Theorem	r1sdom 8915	Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → (𝑅1‘𝐵) ≺ (𝑅1‘𝐴))
Theorem	r111 8916	The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013.)
⊢ 𝑅1:On–1-1→V
Theorem	r1tr 8917	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ Tr (𝑅1‘𝐴)
Theorem	r1tr2 8918	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 8919	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 8920	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 8921	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 8922	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 8923	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 8924	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 8925	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
Theorem	r1sscl 8926	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐶 ⊆ 𝐴) → 𝐶 ∈ (𝑅1‘𝐵))
Theorem	r1val1 8927*	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 8928*	Lemma for tz9.12 8931. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ (𝐹 “ 𝐴) ⊆ On
Theorem	tz9.12lem2 8929*	Lemma for tz9.12 8931. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ suc ∪ (𝐹 “ 𝐴) ∈ On
Theorem	tz9.12lem3 8930*	Lemma for tz9.12 8931. (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 8931*	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 8928 through tz9.12lem3 8930. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘𝑦))
Theorem	tz9.13 8932*	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 8933*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 8932 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥))
Theorem	rankwflemb 8934*	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 8935	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 8936	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 8937	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 8938*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 8957 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 8939	One direction of rankr1a 8977. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → (rank‘𝐴) ∈ 𝐵)
Theorem	rankvaln 8940	Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 8954, unless 𝐴 is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (¬ 𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∅)
Theorem	rankidb 8941	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 8942	A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (rank‘𝐴) ∈ dom 𝑅1
Theorem	rankr1ag 8943	A version of rankr1a 8977 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 8944	A relationship between rank and 𝑅1. See rankr1ag 8943 for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
Theorem	r1rankidb 8945	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 8946	The range of the 𝑅1 function is transitive. Lemma 2.10 of [Kunen] p. 97. One direction of r1elss 8947 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 8947	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 8948	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 8949	A subset of a well-founded set is well-founded. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ ∪ (𝑅1 “ On))
Theorem	snwf 8950	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 8951	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 8952	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 8953	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 8954	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 8955	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 8956*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 8933 is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Theorem	rankval 8957*	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 8958*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 8957 expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
Theorem	rankval2 8959*	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 8960	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 8961	Lemma for rankr1c 8962. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴)))
Theorem	rankr1c 8962	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 8963	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 8964	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 8965	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 8966	A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 8772. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ 𝐴)
Theorem	rankval3b 8967*	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 8968	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 8969	Lemma for rankonid 8970. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝐴 ∈ ∪ (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴))
Theorem	rankonid 8970	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 8971	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 8972	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 8973	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 8974	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 8975	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 8976	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 8977	A relationship between rank and 𝑅1, clearly equivalent to ssrankr1 8976 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 9005 for the subset version. (Contributed by Raph Levien, 29-May-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵))
Theorem	r1val2 8978*	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 8979*	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 8980	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 8981*	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 8982*	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 8983*	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 8984	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 8985	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 8986	A stronger property of 𝑅1 than rankpw 8984. 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 8987	Alternate shorter proof of r1pw 8986 based on the additional axioms ax-reg 8767 and ax-inf2 8816. (Contributed by Raph Levien, 29-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵)))
Theorem	r1pwcl 8988	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 8989	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 8990	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 8991	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 8992	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 8993	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 8994*	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 8995	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 8996*	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 8997	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 8998	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 8999	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 9000	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‘𝐴)))