Definition df-rank 9769

Description: Define the rank function. The rank of a set is the smallest ordinal such that the stage of the cumulative hierarchy of sets at that ordinal includes that set, or equivalently the smallest ordinal such that the stage of the cumulative hierarchy of sets at the successor of that ordinal contains that set. This definition uses that second characterization, while the first is proven in rankval2 9827.

See rankval 9825, rankval2 9827, rankval3 9853, or rankval4 9884 for its value. The rank is therefore a kind of "inverse" of the cumulative hierarchy of sets function, in a sense made precise in rankid 9845 and rankr1a 9848.

Based on Definition 9.14 of [TakeutiZaring] p. 79. (Contributed by NM, 11-Oct-2003.)

Assertion

Ref	Expression
df-rank	⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-rank

Step	Hyp	Ref	Expression
1		crnk 9767	. 2 class rank
2		vx	. . 3 setvar 𝑥
3		cvv 3451	. . 3 class V
4	2	cv 1569	. . . . . 6 class 𝑥
5		vy	. . . . . . . . 9 setvar 𝑦
6	5	cv 1569	. . . . . . . 8 class 𝑦
7	6	csuc 6364	. . . . . . 7 class suc 𝑦
8		cr1 9766	. . . . . . 7 class 𝑅1
9	7, 8	cfv 6538	. . . . . 6 class (𝑅1‘suc 𝑦)
10	4, 9	wcel 2145	. . . . 5 wff 𝑥 ∈ (𝑅1‘suc 𝑦)
11		con0 6362	. . . . 5 class On
12	10, 5, 11	crab 3413	. . . 4 class {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
13	12	cint 4907	. . 3 class ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
14	2, 3, 13	cmpt 5186	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
15	1, 14	wceq 1570	1 wff rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})

This definition is used by:  rankf  9802  rankvalb  9805