![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-rank | Unicode version |
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.) |
Ref | Expression |
---|---|
df-rank |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crnk 8202 | . 2 | |
2 | vx | . . 3 | |
3 | cvv 3109 | . . 3 | |
4 | 2 | cv 1394 | . . . . . 6 |
5 | vy | . . . . . . . . 9 | |
6 | 5 | cv 1394 | . . . . . . . 8 |
7 | 6 | csuc 4885 | . . . . . . 7 |
8 | cr1 8201 | . . . . . . 7 | |
9 | 7, 8 | cfv 5593 | . . . . . 6 |
10 | 4, 9 | wcel 1818 | . . . . 5 |
11 | con0 4883 | . . . . 5 | |
12 | 10, 5, 11 | crab 2811 | . . . 4 |
13 | 12 | cint 4286 | . . 3 |
14 | 2, 3, 13 | cmpt 4510 | . 2 |
15 | 1, 14 | wceq 1395 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: rankf 8233 rankvalb 8236 |
Copyright terms: Public domain | W3C validator |