Metamath Proof Explorer


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 )