Definition df-rank 3488

Description: Define the rank function. See rankval 3512, rankval2 3514, or rankval3 3525 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function R₁: 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 3516 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 3521.

Assertion

Ref	Expression
df-rank	⊢ rank = {⟨x, y⟩∣y = ∩{z ∈ On∣x ∈ (R1 ‘suc z)}}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-rank

Step	Hyp	Ref	Expression
1		crnk 3486	. 2 class rank
2		vy	. . . . 5 set y
3	2	cv 1089	. . . 4 class y
4		vx	. . . . . . . 8 set x
5	4	cv 1089	. . . . . . 7 class x
6		vz	. . . . . . . . . 10 set z
7	6	cv 1089	. . . . . . . . 9 class z
8	7	csuc 2201	. . . . . . . 8 class suc z
9		cr1 3485	. . . . . . . 8 class R1
10	8, 9	cfv 2422	. . . . . . 7 class (R1 ‘suc z)
11	5, 10	wcel 1092	. . . . . 6 wff x ∈ (R1 ‘suc z)
12		con0 2199	. . . . . 6 class On
13	11, 6, 12	crab 1204	. . . . 5 class {z ∈ On∣x ∈ (R1 ‘suc z)}
14	13	cint 1965	. . . 4 class ∩{z ∈ On∣x ∈ (R1 ‘suc z)}
15	3, 14	wceq 1091	. . 3 wff y = ∩{z ∈ On∣x ∈ (R1 ‘suc z)}
16	15, 4, 2	copab 2055	. 2 class {⟨x, y⟩∣y = ∩{z ∈ On∣x ∈ (R1 ‘suc z)}}
17	1, 16	wceq 1091	1 wff rank = {⟨x, y⟩∣y = ∩{z ∈ On∣x ∈ (R1 ‘suc z)}}

This definition is referenced by:  rankval 3512

metamath.org