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 ) |
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 ) |