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

Definition df-rank 8204
Description: Define the rank function. See rankval 8255, rankval2 8257, rankval3 8279, or rankval4 8306 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function : 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 8272 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 8275. (Contributed by NM, 11-Oct-2003.)
Assertion
Ref Expression
df-rank
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-rank
StepHypRef Expression
1 crnk 8202 . 2
2 vx . . 3
3 cvv 3109 . . 3
42cv 1394 . . . . . 6
5 vy . . . . . . . . 9
65cv 1394 . . . . . . . 8
76csuc 4885 . . . . . . 7
8 cr1 8201 . . . . . . 7
97, 8cfv 5593 . . . . . 6
104, 9wcel 1818 . . . . 5
11 con0 4883 . . . . 5
1210, 5, 11crab 2811 . . . 4
1312cint 4286 . . 3
142, 3, 13cmpt 4510 . 2
151, 14wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  rankf  8233  rankvalb  8236
  Copyright terms: Public domain W3C validator