Theorem fnfzo0hashnn0

Description: The value of the size function on a half-open range of nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021)

	Ref	Expression
Assertion	fnfzo0hashnn0	⊢ ( 𝐹 Fn ( 0 ..^ 𝑁 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		hashfn	⊢ ( 𝐹 Fn ( 0 ..^ 𝑁 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
2		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
3		hashcl	⊢ ( ( 0 ..^ 𝑁 ) ∈ Fin → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ∈ ℕ0 )
4	2 3	ax-mp	⊢ ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ∈ ℕ0
5	1 4	eqeltrdi	⊢ ( 𝐹 Fn ( 0 ..^ 𝑁 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )