Theorem fnfz0hashnn0

Description: The size of a function on a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021)

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

Proof

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