Metamath Proof Explorer


Theorem fseq1hash

Description: The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion fseq1hash
|- ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( # ` F ) = N )

Proof

Step Hyp Ref Expression
1 hashfn
 |-  ( F Fn ( 1 ... N ) -> ( # ` F ) = ( # ` ( 1 ... N ) ) )
2 hashfz1
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
3 1 2 sylan9eqr
 |-  ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( # ` F ) = N )