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	$$⊢FFn\left(0\dots N\right)\to \left|F\right|\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		hashfn	$$⊢FFn\left(0\dots N\right)\to \left|F\right|=\left|\left(0\dots N\right)\right|$$
2		fzfi	$$⊢\left(0\dots N\right)\in \mathrm{Fin}$$
3		hashcl	$$⊢\left(0\dots N\right)\in \mathrm{Fin}\to \left|\left(0\dots N\right)\right|\in {\mathbb{N}}_0$$
4	2 3	ax-mp	$$⊢\left|\left(0\dots N\right)\right|\in {\mathbb{N}}_0$$
5	1 4	eqeltrdi	$$⊢FFn\left(0\dots N\right)\to \left|F\right|\in {\mathbb{N}}_0$$