Theorem hashnemnf

Description: The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017)

	Ref	Expression
Assertion	hashnemnf	$$⊢A\in V\to \left|A\right|\ne \mathrm{-\infty }$$

Proof

Step	Hyp	Ref	Expression
1		hashnn0pnf	$$⊢A\in V\to \left(\left|A\right|\in {\mathbb{N}}_0\vee \left|A\right|=\mathrm{+\infty }\right)$$
2		mnfnre	$$⊢\mathrm{-\infty }\notin ℝ$$
3		df-nel	$$⊢\mathrm{-\infty }\notin ℝ\leftrightarrow \neg \mathrm{-\infty }\in ℝ$$
4		nn0re	$$⊢\mathrm{-\infty }\in {\mathbb{N}}_0\to \mathrm{-\infty }\in ℝ$$
5	4	con3i	$$⊢\neg \mathrm{-\infty }\in ℝ\to \neg \mathrm{-\infty }\in {\mathbb{N}}_0$$
6	3 5	sylbi	$$⊢\mathrm{-\infty }\notin ℝ\to \neg \mathrm{-\infty }\in {\mathbb{N}}_0$$
7	2 6	ax-mp	$$⊢\neg \mathrm{-\infty }\in {\mathbb{N}}_0$$
8		eleq1	$$⊢\left|A\right|=\mathrm{-\infty }\to \left(\left|A\right|\in {\mathbb{N}}_0\leftrightarrow \mathrm{-\infty }\in {\mathbb{N}}_0\right)$$
9	7 8	mtbiri	$$⊢\left|A\right|=\mathrm{-\infty }\to \neg \left|A\right|\in {\mathbb{N}}_0$$
10	9	necon2ai	$$⊢\left|A\right|\in {\mathbb{N}}_0\to \left|A\right|\ne \mathrm{-\infty }$$
11		pnfnemnf	$$⊢\mathrm{+\infty }\ne \mathrm{-\infty }$$
12		neeq1	$$⊢\left|A\right|=\mathrm{+\infty }\to \left(\left|A\right|\ne \mathrm{-\infty }\leftrightarrow \mathrm{+\infty }\ne \mathrm{-\infty }\right)$$
13	11 12	mpbiri	$$⊢\left|A\right|=\mathrm{+\infty }\to \left|A\right|\ne \mathrm{-\infty }$$
14	10 13	jaoi	$$⊢\left(\left|A\right|\in {\mathbb{N}}_0\vee \left|A\right|=\mathrm{+\infty }\right)\to \left|A\right|\ne \mathrm{-\infty }$$
15	1 14	syl	$$⊢A\in V\to \left|A\right|\ne \mathrm{-\infty }$$