Definition df-rank 7993

Description: Define the rank function. See rankval 8044, rankval2 8046, rankval3 8068, or rankval4 8095 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function R1: 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 8061 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 8064. (Contributed by NM, 11-Oct-2003.)

Assertion

Ref	Expression
df-rank	|- rank = ( x e. _V |-> |^| { y e. On | x e. ( R1 ` suc y ) } )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-rank

Step	Hyp	Ref	Expression
1		crnk 7991	. 2 class rank
2		vx	. . 3 setvar x
3		cvv 2993	. . 3 class _V
4	2	cv 1368	. . . . . 6 class x
5		vy	. . . . . . . . 9 setvar y
6	5	cv 1368	. . . . . . . 8 class y
7	6	csuc 4742	. . . . . . 7 class suc y
8		cr1 7990	. . . . . . 7 class R1
9	7, 8	cfv 5439	. . . . . 6 class ( R1 ` suc y )
10	4, 9	wcel 1756	. . . . 5 wff x e. ( R1 ` suc y )
11		con0 4740	. . . . 5 class On
12	10, 5, 11	crab 2740	. . . 4 class { y e. On | x e. ( R1 ` suc y ) }
13	12	cint 4149	. . 3 class |^| { y e. On | x e. ( R1 ` suc y ) }
14	2, 3, 13	cmpt 4371	. 2 class ( x e. _V |-> |^| { y e. On | x e. ( R1 ` suc y ) } )
15	1, 14	wceq 1369	1 wff rank = ( x e. _V |-> |^| { y e. On | x e. ( R1 ` suc y ) } )

This definition is referenced by:  rankf  8022  rankvalb  8025