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 F Fn 0 N F 0

Proof

Step Hyp Ref Expression
1 hashfn F Fn 0 N F = 0 N
2 fzfi 0 N Fin
3 hashcl 0 N Fin 0 N 0
4 2 3 ax-mp 0 N 0
5 1 4 eqeltrdi F Fn 0 N F 0