Metamath Proof Explorer


Theorem rankf

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 rank:R1OnOn

Proof

Step Hyp Ref Expression
1 df-rank rank=xVyOn|xR1sucy
2 1 funmpt2 Funrank
3 mptv xVyOn|xR1sucy=xz|z=yOn|xR1sucy
4 1 3 eqtri rank=xz|z=yOn|xR1sucy
5 4 dmeqi domrank=domxz|z=yOn|xR1sucy
6 dmopab domxz|z=yOn|xR1sucy=x|zz=yOn|xR1sucy
7 abeq1 x|zz=yOn|xR1sucy=R1Onxzz=yOn|xR1sucyxR1On
8 rankwflemb xR1OnyOnxR1sucy
9 intexrab yOnxR1sucyyOn|xR1sucyV
10 isset yOn|xR1sucyVzz=yOn|xR1sucy
11 8 9 10 3bitrri zz=yOn|xR1sucyxR1On
12 7 11 mpgbir x|zz=yOn|xR1sucy=R1On
13 6 12 eqtri domxz|z=yOn|xR1sucy=R1On
14 5 13 eqtri domrank=R1On
15 df-fn rankFnR1OnFunrankdomrank=R1On
16 2 14 15 mpbir2an rankFnR1On
17 rabn0 yOn|xR1sucyyOnxR1sucy
18 8 17 bitr4i xR1OnyOn|xR1sucy
19 intex yOn|xR1sucyyOn|xR1sucyV
20 vex xV
21 1 fvmpt2 xVyOn|xR1sucyVrankx=yOn|xR1sucy
22 20 21 mpan yOn|xR1sucyVrankx=yOn|xR1sucy
23 19 22 sylbi yOn|xR1sucyrankx=yOn|xR1sucy
24 ssrab2 yOn|xR1sucyOn
25 oninton yOn|xR1sucyOnyOn|xR1sucyyOn|xR1sucyOn
26 24 25 mpan yOn|xR1sucyyOn|xR1sucyOn
27 23 26 eqeltrd yOn|xR1sucyrankxOn
28 18 27 sylbi xR1OnrankxOn
29 28 rgen xR1OnrankxOn
30 ffnfv rank:R1OnOnrankFnR1OnxR1OnrankxOn
31 16 29 30 mpbir2an rank:R1OnOn