Theorem hashxnn0

Description: The value of the hash function for a set is an extended nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 10-Dec-2020)

	Ref	Expression
Assertion	hashxnn0	$$⊢M\in V\to \left|M\right|\in {\mathbb{N}}_0^{*}$$

Proof

Step	Hyp	Ref	Expression
1		hashfxnn0	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}$$
2	1	a1i	$$⊢M\in V\to \left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}$$
3		elex	$$⊢M\in V\to M\in \mathrm{V}$$
4	2 3	ffvelrnd	$$⊢M\in V\to \left|M\right|\in {\mathbb{N}}_0^{*}$$