Metamath Proof Explorer

Theorem hashcard

Description: The size function of the cardinality function. (Contributed by Mario Carneiro, 19-Sep-2013) (Revised by Mario Carneiro, 4-Nov-2013)

Ref Expression
Assertion hashcard 
|- ( A e. Fin -> ( # ` ( card ` A ) ) = ( # ` A ) )

Proof

Step Hyp Ref Expression
1 cardidm 
 |-  ( card ` ( card ` A ) ) = ( card ` A )
2 1 fveq2i 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( card ` A ) ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) )
3 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
4 ssid 
 |-  ( card ` A ) C_ ( card ` A )
5 ssnnfi 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` A ) C_ ( card ` A ) ) -> ( card ` A ) e. Fin )
6 3 4 5 sylancl 
 |-  ( A e. Fin -> ( card ` A ) e. Fin )
7 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
8 7 hashgval 
 |-  ( ( card ` A ) e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( card ` A ) ) ) = ( # ` ( card ` A ) ) )
9 6 8 syl 
 |-  ( A e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( card ` A ) ) ) = ( # ` ( card ` A ) ) )
10 7 hashgval 
 |-  ( A e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( # ` A ) )
11 2 9 10 3eqtr3a 
 |-  ( A e. Fin -> ( # ` ( card ` A ) ) = ( # ` A ) )