Theorem ffz0hash

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	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶B\right)\to \left|F\right|=N+1$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢F:\left(0\dots N\right)⟶B\to FFn\left(0\dots N\right)$$
2		fnfz0hash	$$⊢\left(N\in {\mathbb{N}}_0\wedge FFn\left(0\dots N\right)\right)\to \left|F\right|=N+1$$
3	1 2	sylan2	$$⊢\left(N\in {\mathbb{N}}_0\wedge F:\left(0\dots N\right)⟶B\right)\to \left|F\right|=N+1$$