Metamath Proof Explorer


Definition df-rank

Description: Define the rank function. See rankval , rankval2 , rankval3 , or rankval4 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 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a . (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 ) } )