Definition df-rank 9782

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 9840.

See rankval 9838, rankval2 9840, rankval3 9866, or rankval4 9897 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 9858 and rankr1a 9861.

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 9780	. 2 class rank
2		vx	. . 3 setvar 𝑥
3		cvv 3454	. . 3 class V
4	2	cv 1568	. . . . . 6 class 𝑥
5		vy	. . . . . . . . 9 setvar 𝑦
6	5	cv 1568	. . . . . . . 8 class 𝑦
7	6	csuc 6371	. . . . . . 7 class suc 𝑦
8		cr1 9779	. . . . . . 7 class 𝑅1
9	7, 8	cfv 6547	. . . . . 6 class (𝑅1‘suc 𝑦)
10	4, 9	wcel 2146	. . . . 5 wff 𝑥 ∈ (𝑅1‘suc 𝑦)
11		con0 6369	. . . . 5 class On
12	10, 5, 11	crab 3416	. . . 4 class {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
13	12	cint 4910	. . 3 class ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
14	2, 3, 13	cmpt 5189	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
15	1, 14	wceq 1569	1 wff rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})

This definition is used by:  rankf  9815  rankvalb  9818