Theorem pnf0xnn0

Description: Positive infinity is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	pnf0xnn0	$$⊢\mathrm{+\infty }\in {\mathbb{N}}_0^{*}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{+\infty }=\mathrm{+\infty }$$
2	1	olci	$$⊢\left(\mathrm{+\infty }\in {\mathbb{N}}_0\vee \mathrm{+\infty }=\mathrm{+\infty }\right)$$
3		elxnn0	$$⊢\mathrm{+\infty }\in {\mathbb{N}}_0^{*}\leftrightarrow \left(\mathrm{+\infty }\in {\mathbb{N}}_0\vee \mathrm{+\infty }=\mathrm{+\infty }\right)$$
4	2 3	mpbir	$$⊢\mathrm{+\infty }\in {\mathbb{N}}_0^{*}$$