Metamath Proof Explorer

Theorem hashgval2

Description: A short expression for the G function of hashgf1o . (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Assertion hashgval2 
|- ( # |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )

Proof

Step Hyp Ref Expression
1 hashresfn 
 |-  ( # |` _om ) Fn _om
2 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) Fn _om
3 eqfnfv 
 |-  ( ( ( # |` _om ) Fn _om /\ ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) Fn _om ) -> ( ( # |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) <-> A. y e. _om ( ( # |` _om ) ` y ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` y ) ) )
4 1 2 3 mp2an 
 |-  ( ( # |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) <-> A. y e. _om ( ( # |` _om ) ` y ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` y ) )
5 fvres 
 |-  ( y e. _om -> ( ( # |` _om ) ` y ) = ( # ` y ) )
6 nnfi 
 |-  ( y e. _om -> y e. Fin )
7 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
8 7 hashgval 
 |-  ( y e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` y ) ) = ( # ` y ) )
9 6 8 syl 
 |-  ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` y ) ) = ( # ` y ) )
10 cardnn 
 |-  ( y e. _om -> ( card ` y ) = y )
11 10 fveq2d 
 |-  ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` y ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` y ) )
12 5 9 11 3eqtr2d 
 |-  ( y e. _om -> ( ( # |` _om ) ` y ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` y ) )
13 4 12 mprgbir 
 |-  ( # |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )