Metamath Proof Explorer

Theorem hashkf

Description: The finite part of the size function maps all finite sets to their cardinality, as members of NN0 . (Contributed by Mario Carneiro, 13-Sep-2013) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses hashgval.1 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
hashkf.2 
|- K = ( G o. card )
Assertion hashkf 
|- K : Fin --> NN0

Proof

Step Hyp Ref Expression
1 hashgval.1 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2 hashkf.2 
 |-  K = ( G o. card )
3 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) Fn _om
4 1 fneq1i 
 |-  ( G Fn _om <-> ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) Fn _om )
5 3 4 mpbir 
 |-  G Fn _om
6 fnfun 
 |-  ( G Fn _om -> Fun G )
7 5 6 ax-mp 
 |-  Fun G
8 cardf2 
 |-  card : { y | E. x e. On x ~~ y } --> On
9 ffun 
 |-  ( card : { y | E. x e. On x ~~ y } --> On -> Fun card )
10 8 9 ax-mp 
 |-  Fun card
11 funco 
 |-  ( ( Fun G /\ Fun card ) -> Fun ( G o. card ) )
12 7 10 11 mp2an 
 |-  Fun ( G o. card )
13 dmco 
 |-  dom ( G o. card ) = ( `' card " dom G )
14 5 fndmi 
 |-  dom G = _om
15 14 imaeq2i 
 |-  ( `' card " dom G ) = ( `' card " _om )
16 funfn 
 |-  ( Fun card <-> card Fn dom card )
17 10 16 mpbi 
 |-  card Fn dom card
18 elpreima 
 |-  ( card Fn dom card -> ( y e. ( `' card " _om ) <-> ( y e. dom card /\ ( card ` y ) e. _om ) ) )
19 17 18 ax-mp 
 |-  ( y e. ( `' card " _om ) <-> ( y e. dom card /\ ( card ` y ) e. _om ) )
20 id 
 |-  ( ( card ` y ) e. _om -> ( card ` y ) e. _om )
21 cardid2 
 |-  ( y e. dom card -> ( card ` y ) ~~ y )
22 21 ensymd 
 |-  ( y e. dom card -> y ~~ ( card ` y ) )
23 breq2 
 |-  ( x = ( card ` y ) -> ( y ~~ x <-> y ~~ ( card ` y ) ) )
24 23 rspcev 
 |-  ( ( ( card ` y ) e. _om /\ y ~~ ( card ` y ) ) -> E. x e. _om y ~~ x )
25 20 22 24 syl2anr 
 |-  ( ( y e. dom card /\ ( card ` y ) e. _om ) -> E. x e. _om y ~~ x )
26 isfi 
 |-  ( y e. Fin <-> E. x e. _om y ~~ x )
27 25 26 sylibr 
 |-  ( ( y e. dom card /\ ( card ` y ) e. _om ) -> y e. Fin )
28 finnum 
 |-  ( y e. Fin -> y e. dom card )
29 ficardom 
 |-  ( y e. Fin -> ( card ` y ) e. _om )
30 28 29 jca 
 |-  ( y e. Fin -> ( y e. dom card /\ ( card ` y ) e. _om ) )
31 27 30 impbii 
 |-  ( ( y e. dom card /\ ( card ` y ) e. _om ) <-> y e. Fin )
32 19 31 bitri 
 |-  ( y e. ( `' card " _om ) <-> y e. Fin )
33 32 eqriv 
 |-  ( `' card " _om ) = Fin
34 13 15 33 3eqtri 
 |-  dom ( G o. card ) = Fin
35 df-fn 
 |-  ( ( G o. card ) Fn Fin <-> ( Fun ( G o. card ) /\ dom ( G o. card ) = Fin ) )
36 12 34 35 mpbir2an 
 |-  ( G o. card ) Fn Fin
37 2 fneq1i 
 |-  ( K Fn Fin <-> ( G o. card ) Fn Fin )
38 36 37 mpbir 
 |-  K Fn Fin
39 2 fveq1i 
 |-  ( K ` y ) = ( ( G o. card ) ` y )
40 fvco 
 |-  ( ( Fun card /\ y e. dom card ) -> ( ( G o. card ) ` y ) = ( G ` ( card ` y ) ) )
41 10 28 40 sylancr 
 |-  ( y e. Fin -> ( ( G o. card ) ` y ) = ( G ` ( card ` y ) ) )
42 39 41 syl5eq 
 |-  ( y e. Fin -> ( K ` y ) = ( G ` ( card ` y ) ) )
43 1 hashgf1o 
 |-  G : _om -1-1-onto-> NN0
44 f1of 
 |-  ( G : _om -1-1-onto-> NN0 -> G : _om --> NN0 )
45 43 44 ax-mp 
 |-  G : _om --> NN0
46 45 ffvelrni 
 |-  ( ( card ` y ) e. _om -> ( G ` ( card ` y ) ) e. NN0 )
47 29 46 syl 
 |-  ( y e. Fin -> ( G ` ( card ` y ) ) e. NN0 )
48 42 47 eqeltrd 
 |-  ( y e. Fin -> ( K ` y ) e. NN0 )
49 48 rgen 
 |-  A. y e. Fin ( K ` y ) e. NN0
50 ffnfv 
 |-  ( K : Fin --> NN0 <-> ( K Fn Fin /\ A. y e. Fin ( K ` y ) e. NN0 ) )
51 38 49 50 mpbir2an 
 |-  K : Fin --> NN0