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