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

Proof

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