Theorem hashnn0pnf

Description: The value of the hash function for a set is either a nonnegative integer or positive infinity. TODO-AV: mark as OBSOLETE and replace it by hashxnn0 ? (Contributed by Alexander van der Vekens, 6-Dec-2017)

	Ref	Expression
Assertion	hashnn0pnf	$$⊢M\in V\to \left(\left|M\right|\in {\mathbb{N}}_0\vee \left|M\right|=\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
2	1	a1i	$$⊢M\in V\to \left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
3		elex	$$⊢M\in V\to M\in \mathrm{V}$$
4	2 3	ffvelrnd	$$⊢M\in V\to \left|M\right|\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)$$
5		elun	$$⊢\left|M\right|\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)\leftrightarrow \left(\left|M\right|\in {\mathbb{N}}_0\vee \left|M\right|\in \left\{\mathrm{+\infty }\right\}\right)$$
6		elsni	$$⊢\left|M\right|\in \left\{\mathrm{+\infty }\right\}\to \left|M\right|=\mathrm{+\infty }$$
7	6	orim2i	$$⊢\left(\left|M\right|\in {\mathbb{N}}_0\vee \left|M\right|\in \left\{\mathrm{+\infty }\right\}\right)\to \left(\left|M\right|\in {\mathbb{N}}_0\vee \left|M\right|=\mathrm{+\infty }\right)$$
8	5 7	sylbi	$$⊢\left|M\right|\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)\to \left(\left|M\right|\in {\mathbb{N}}_0\vee \left|M\right|=\mathrm{+\infty }\right)$$
9	4 8	syl	$$⊢M\in V\to \left(\left|M\right|\in {\mathbb{N}}_0\vee \left|M\right|=\mathrm{+\infty }\right)$$