MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rank Structured version   Visualization version   Unicode version

Definition df-rank 8254
Description: Define the rank function. See rankval 8305, rankval2 8307, rankval3 8329, or rankval4 8356 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 8322 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 8325. (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
StepHypRef Expression
1 crnk 8252 . 2  class  rank
2 vx . . 3  setvar  x
3 cvv 3031 . . 3  class  _V
42cv 1451 . . . . . 6  class  x
5 vy . . . . . . . . 9  setvar  y
65cv 1451 . . . . . . . 8  class  y
76csuc 5432 . . . . . . 7  class  suc  y
8 cr1 8251 . . . . . . 7  class  R1
97, 8cfv 5589 . . . . . 6  class  ( R1
`  suc  y )
104, 9wcel 1904 . . . . 5  wff  x  e.  ( R1 `  suc  y )
11 con0 5430 . . . . 5  class  On
1210, 5, 11crab 2760 . . . 4  class  { y  e.  On  |  x  e.  ( R1 `  suc  y ) }
1312cint 4226 . . 3  class  |^| { y  e.  On  |  x  e.  ( R1 `  suc  y ) }
142, 3, 13cmpt 4454 . 2  class  ( x  e.  _V  |->  |^| { y  e.  On  |  x  e.  ( R1 `  suc  y ) } )
151, 14wceq 1452 1  wff  rank  =  ( x  e.  _V  |->  |^|
{ y  e.  On  |  x  e.  ( R1 `  suc  y ) } )
Colors of variables: wff setvar class
This definition is referenced by:  rankf  8283  rankvalb  8286
  Copyright terms: Public domain W3C validator