Metamath Proof Explorer

Theorem hashfz1

Description: The set ( 1 ... N ) has N elements. (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion hashfz1 
|- ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )

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 cardfz 
 |-  ( N e. NN0 -> ( card ` ( 1 ... N ) ) = ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` N ) )
3 2 fveq2d 
 |-  ( N e. NN0 -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... N ) ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` N ) ) )
4 fzfid 
 |-  ( N e. NN0 -> ( 1 ... N ) e. Fin )
5 1 hashgval 
 |-  ( ( 1 ... N ) e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... N ) ) ) = ( # ` ( 1 ... N ) ) )
6 4 5 syl 
 |-  ( N e. NN0 -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... N ) ) ) = ( # ` ( 1 ... N ) ) )
7 1 hashgf1o 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0
8 f1ocnvfv2 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0 /\ N e. NN0 ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` N ) ) = N )
9 7 8 mpan 
 |-  ( N e. NN0 -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` N ) ) = N )
10 3 6 9 3eqtr3d 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )