Theorem fnfz0hash

Description: The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018)

	Ref	Expression
Assertion	fnfz0hash	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 0 ... 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = ( 𝑁 + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		hashfn	⊢ ( 𝐹 Fn ( 0 ... 𝑁 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ( 0 ... 𝑁 ) ) )
2		hashfz0	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝑁 ) ) = ( 𝑁 + 1 ) )
3	1 2	sylan9eqr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 0 ... 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = ( 𝑁 + 1 ) )