Description: The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018) (Proof shortened by AV, 11-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | ffz0hash | |- ( ( N e. NN0 /\ F : ( 0 ... N ) --> B ) -> ( # ` F ) = ( N + 1 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn | |- ( F : ( 0 ... N ) --> B -> F Fn ( 0 ... N ) ) |
|
2 | fnfz0hash | |- ( ( N e. NN0 /\ F Fn ( 0 ... N ) ) -> ( # ` F ) = ( N + 1 ) ) |
|
3 | 1 2 | sylan2 | |- ( ( N e. NN0 /\ F : ( 0 ... N ) --> B ) -> ( # ` F ) = ( N + 1 ) ) |