Definition df-rank 9805

Description: Define the rank function. See rankval 9856, rankval2 9858, rankval3 9880, or rankval4 9907 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function 𝑅₁: 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 9873 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 9876. (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 9803	. 2 class rank
2		vx	. . 3 setvar 𝑥
3		cvv 3480	. . 3 class V
4	2	cv 1539	. . . . . 6 class 𝑥
5		vy	. . . . . . . . 9 setvar 𝑦
6	5	cv 1539	. . . . . . . 8 class 𝑦
7	6	csuc 6386	. . . . . . 7 class suc 𝑦
8		cr1 9802	. . . . . . 7 class 𝑅1
9	7, 8	cfv 6561	. . . . . 6 class (𝑅1‘suc 𝑦)
10	4, 9	wcel 2108	. . . . 5 wff 𝑥 ∈ (𝑅1‘suc 𝑦)
11		con0 6384	. . . . 5 class On
12	10, 5, 11	crab 3436	. . . 4 class {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
13	12	cint 4946	. . 3 class ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
14	2, 3, 13	cmpt 5225	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
15	1, 14	wceq 1540	1 wff rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})

This definition is referenced by:  rankf  9834  rankvalb  9837