Metamath Proof Explorer

Theorem hashcl

Description: Closure of the # function. (Contributed by Paul Chapman, 26-Oct-2012) (Revised by Mario Carneiro, 13-Jul-2014)

Ref Expression
Assertion hashcl 
|- ( A e. Fin -> ( # ` A ) e. NN0 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2 1 hashgval 
 |-  ( A e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( # ` A ) )
3 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
4 1 hashgf1o 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0
5 f1of 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0 -> ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om --> NN0 )
6 4 5 ax-mp 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om --> NN0
7 6 ffvelcdmi 
 |-  ( ( card ` A ) e. _om -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) e. NN0 )
8 3 7 syl 
 |-  ( A e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) e. NN0 )
9 2 8 eqeltrrd 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )