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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 ) → ( ♯ ‘ 𝐹 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 → 𝐹 Fn ( 0 ..^ 𝑁 ) )
2		ffzo0hash	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
3	1 2	sylan2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 ) → ( ♯ ‘ 𝐹 ) = 𝑁 )