Definition df-rank

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 .

See rankval , rankval2 , rankval3 , or rankval4 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 and rankr1a .

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crnk	|- rank
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4		con0	|- On
5	1	cv	|- x
6		cr1	|- R1
7	3	cv	|- y
8	7	csuc	|- suc y
9	8 6	cfv	|- ( R1 ` suc y )
10	5 9	wcel	|- x e. ( R1 ` suc y )
11	10 3 4	crab	|- { y e. On | x e. ( R1 ` suc y ) }
12	11	cint	|- |^| { y e. On | x e. ( R1 ` suc y ) }
13	1 2 12	cmpt	|- ( x e. _V |-> |^| { y e. On | x e. ( R1 ` suc y ) } )
14	0 13	wceq	|- rank = ( x e. _V |-> |^| { y e. On | x e. ( R1 ` suc y ) } )