Description: The domain and range of the rank function. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 12-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | rankf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rank | |
|
2 | 1 | funmpt2 | |
3 | mptv | |
|
4 | 1 3 | eqtri | |
5 | 4 | dmeqi | |
6 | dmopab | |
|
7 | abeq1 | |
|
8 | rankwflemb | |
|
9 | intexrab | |
|
10 | isset | |
|
11 | 8 9 10 | 3bitrri | |
12 | 7 11 | mpgbir | |
13 | 6 12 | eqtri | |
14 | 5 13 | eqtri | |
15 | df-fn | |
|
16 | 2 14 15 | mpbir2an | |
17 | rabn0 | |
|
18 | 8 17 | bitr4i | |
19 | intex | |
|
20 | vex | |
|
21 | 1 | fvmpt2 | |
22 | 20 21 | mpan | |
23 | 19 22 | sylbi | |
24 | ssrab2 | |
|
25 | oninton | |
|
26 | 24 25 | mpan | |
27 | 23 26 | eqeltrd | |
28 | 18 27 | sylbi | |
29 | 28 | rgen | |
30 | ffnfv | |
|
31 | 16 29 30 | mpbir2an | |