Theorem nn0nepnf

Description: No standard nonnegative integer equals positive infinity. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	nn0nepnf	$$⊢A\in {\mathbb{N}}_0\to A\ne \mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		pnfnre	$$⊢\mathrm{+\infty }\notin ℝ$$
2	1	neli	$$⊢\neg \mathrm{+\infty }\in ℝ$$
3		nn0re	$$⊢\mathrm{+\infty }\in {\mathbb{N}}_0\to \mathrm{+\infty }\in ℝ$$
4	2 3	mto	$$⊢\neg \mathrm{+\infty }\in {\mathbb{N}}_0$$
5		eleq1	$$⊢A=\mathrm{+\infty }\to \left(A\in {\mathbb{N}}_0\leftrightarrow \mathrm{+\infty }\in {\mathbb{N}}_0\right)$$
6	4 5	mtbiri	$$⊢A=\mathrm{+\infty }\to \neg A\in {\mathbb{N}}_0$$
7	6	necon2ai	$$⊢A\in {\mathbb{N}}_0\to A\ne \mathrm{+\infty }$$