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 disjdifr 
 |-  ( ( _V \ Fin ) i^i Fin ) = (/)
10 pnfex 
 |-  +oo e. _V
11 10 fconst 
 |-  ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo }
12 ffn 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo } -> ( ( _V \ Fin ) X. { +oo } ) Fn ( _V \ Fin ) )
13 fnresdisj 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) Fn ( _V \ Fin ) -> ( ( ( _V \ Fin ) i^i Fin ) = (/) <-> ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) = (/) ) )
14 11 12 13 mp2b 
 |-  ( ( ( _V \ Fin ) i^i Fin ) = (/) <-> ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) = (/) )
15 9 14 mpbi 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) |` Fin ) = (/)
16 8 15 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. (/) )
17 un0 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. (/) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
18 16 17 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 )
19 2 18 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 )
20 df-hash 
 |-  # = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )
21 20 reseq1i 
 |-  ( # |` Fin ) = ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) |` Fin )
22 1 coeq1i 
 |-  ( G o. card ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
23 19 21 22 3eqtr4i 
 |-  ( # |` Fin ) = ( G o. card )
24 23 fveq1i 
 |-  ( ( # |` Fin ) ` A ) = ( ( G o. card ) ` A )
25 cardf2 
 |-  card : { x | E. y e. On y ~~ x } --> On
26 ffun 
 |-  ( card : { x | E. y e. On y ~~ x } --> On -> Fun card )
27 25 26 ax-mp 
 |-  Fun card
28 finnum 
 |-  ( A e. Fin -> A e. dom card )
29 fvco 
 |-  ( ( Fun card /\ A e. dom card ) -> ( ( G o. card ) ` A ) = ( G ` ( card ` A ) ) )
30 27 28 29 sylancr 
 |-  ( A e. Fin -> ( ( G o. card ) ` A ) = ( G ` ( card ` A ) ) )
31 24 30 eqtrid 
 |-  ( A e. Fin -> ( ( # |` Fin ) ` A ) = ( G ` ( card ` A ) ) )
32 fvres 
 |-  ( A e. Fin -> ( ( # |` Fin ) ` A ) = ( # ` A ) )
33 31 32 eqtr3d 
 |-  ( A e. Fin -> ( G ` ( card ` A ) ) = ( # ` A ) )