Metamath Proof Explorer


Theorem fnfzo0hash

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 )

Proof

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 )