Metamath Proof Explorer

Theorem hashgval

Description: The value of the # function in terms of the mapping G from _om to NN0 . The proof avoids the use of ax-ac . (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypothesis hashgval.1 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
Assertion hashgval 
|- ( A e. Fin -> ( G ` ( card ` A ) ) = ( # ` A ) )

Proof

Step Hyp Ref Expression
1 hashgval.1 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2 resundir 
 |-  ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) |` Fin ) = ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` Fin ) u. ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) )
3 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
4 eqid 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
5 3 4 hashkf 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) : Fin --> NN0
6 ffn 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) : Fin --> NN0 -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) Fn Fin )
7 fnresdm 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) Fn Fin -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` Fin ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) )
8 5 6 7 mp2b 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` Fin ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
9 incom 
 |-  ( ( _V \ Fin ) i^i Fin ) = ( Fin i^i ( _V \ Fin ) )
10 disjdif 
 |-  ( Fin i^i ( _V \ Fin ) ) = (/)
11 9 10 eqtri 
 |-  ( ( _V \ Fin ) i^i Fin ) = (/)
12 pnfex 
 |-  +oo e. _V
13 12 fconst 
 |-  ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo }
14 ffn 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo } -> ( ( _V \ Fin ) X. { +oo } ) Fn ( _V \ Fin ) )
15 fnresdisj 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) Fn ( _V \ Fin ) -> ( ( ( _V \ Fin ) i^i Fin ) = (/) <-> ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) = (/) ) )
16 13 14 15 mp2b 
 |-  ( ( ( _V \ Fin ) i^i Fin ) = (/) <-> ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) = (/) )
17 11 16 mpbi 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) = (/)
18 8 17 uneq12i 
 |-  ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` Fin ) u. ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. (/) )
19 un0 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. (/) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
20 18 19 eqtri 
 |-  ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` Fin ) u. ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
21 2 20 eqtri 
 |-  ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) |` Fin ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
22 df-hash 
 |-  # = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )
23 22 reseq1i 
 |-  ( # |` Fin ) = ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) |` Fin )
24 1 coeq1i 
 |-  ( G o. card ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
25 21 23 24 3eqtr4i 
 |-  ( # |` Fin ) = ( G o. card )
26 25 fveq1i 
 |-  ( ( # |` Fin ) ` A ) = ( ( G o. card ) ` A )
27 cardf2 
 |-  card : { x | E. y e. On y ~~ x } --> On
28 ffun 
 |-  ( card : { x | E. y e. On y ~~ x } --> On -> Fun card )
29 27 28 ax-mp 
 |-  Fun card
30 finnum 
 |-  ( A e. Fin -> A e. dom card )
31 fvco 
 |-  ( ( Fun card /\ A e. dom card ) -> ( ( G o. card ) ` A ) = ( G ` ( card ` A ) ) )
32 29 30 31 sylancr 
 |-  ( A e. Fin -> ( ( G o. card ) ` A ) = ( G ` ( card ` A ) ) )
33 26 32 syl5eq 
 |-  ( A e. Fin -> ( ( # |` Fin ) ` A ) = ( G ` ( card ` A ) ) )
34 fvres 
 |-  ( A e. Fin -> ( ( # |` Fin ) ` A ) = ( # ` A ) )
35 33 34 eqtr3d 
 |-  ( A e. Fin -> ( G ` ( card ` A ) ) = ( # ` A ) )