Description: The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018) (Proof shortened by AV, 11-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fnfzo0hash | |- ( ( N e. NN0 /\ F : ( 0 ..^ N ) --> B ) -> ( # ` F ) = N ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ffn | |- ( F : ( 0 ..^ N ) --> B -> F Fn ( 0 ..^ N ) ) |
|
| 2 | ffzo0hash | |- ( ( N e. NN0 /\ F Fn ( 0 ..^ N ) ) -> ( # ` F ) = N ) |
|
| 3 | 1 2 | sylan2 | |- ( ( N e. NN0 /\ F : ( 0 ..^ N ) --> B ) -> ( # ` F ) = N ) |