Theorem hashnnn0genn0

Description: If the size of a set is not a nonnegative integer, it is greater than or equal to any nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017)

	Ref	Expression
Assertion	hashnnn0genn0	$$⊢\left(M\in V\wedge \left|M\right|\notin {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N\le \left|M\right|$$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$$⊢\left|M\right|\notin {\mathbb{N}}_0\leftrightarrow \neg \left|M\right|\in {\mathbb{N}}_0$$
2		pm2.21	$$⊢\neg \left|M\right|\in {\mathbb{N}}_0\to \left(\left|M\right|\in {\mathbb{N}}_0\to N\le \left|M\right|\right)$$
3	1 2	sylbi	$$⊢\left|M\right|\notin {\mathbb{N}}_0\to \left(\left|M\right|\in {\mathbb{N}}_0\to N\le \left|M\right|\right)$$
4	3	3ad2ant2	$$⊢\left(M\in V\wedge \left|M\right|\notin {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(\left|M\right|\in {\mathbb{N}}_0\to N\le \left|M\right|\right)$$
5		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
6	5	ltpnfd	$$⊢N\in {\mathbb{N}}_0\to N<\mathrm{+\infty }$$
7	5	rexrd	$$⊢N\in {\mathbb{N}}_0\to N\in {ℝ}^{*}$$
8		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
9		xrltle	$$⊢\left(N\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(N<\mathrm{+\infty }\to N\le \mathrm{+\infty }\right)$$
10	7 8 9	sylancl	$$⊢N\in {\mathbb{N}}_0\to \left(N<\mathrm{+\infty }\to N\le \mathrm{+\infty }\right)$$
11	6 10	mpd	$$⊢N\in {\mathbb{N}}_0\to N\le \mathrm{+\infty }$$
12		breq2	$$⊢\left|M\right|=\mathrm{+\infty }\to \left(N\le \left|M\right|\leftrightarrow N\le \mathrm{+\infty }\right)$$
13	11 12	syl5ibrcom	$$⊢N\in {\mathbb{N}}_0\to \left(\left|M\right|=\mathrm{+\infty }\to N\le \left|M\right|\right)$$
14	13	3ad2ant3	$$⊢\left(M\in V\wedge \left|M\right|\notin {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(\left|M\right|=\mathrm{+\infty }\to N\le \left|M\right|\right)$$
15		hashnn0pnf	$$⊢M\in V\to \left(\left|M\right|\in {\mathbb{N}}_0\vee \left|M\right|=\mathrm{+\infty }\right)$$
16	15	3ad2ant1	$$⊢\left(M\in V\wedge \left|M\right|\notin {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(\left|M\right|\in {\mathbb{N}}_0\vee \left|M\right|=\mathrm{+\infty }\right)$$
17	4 14 16	mpjaod	$$⊢\left(M\in V\wedge \left|M\right|\notin {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N\le \left|M\right|$$