Theorem elxnn0

Description: An extended nonnegative integer is either a standard nonnegative integer or positive infinity. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	elxnn0	$$⊢A\in {\mathbb{N}}_0^{*}\leftrightarrow \left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-xnn0	$$⊢{\mathbb{N}}_0^{*}={\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
2	1	eleq2i	$$⊢A\in {\mathbb{N}}_0^{*}\leftrightarrow A\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)$$
3		elun	$$⊢A\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)\leftrightarrow \left(A\in {\mathbb{N}}_0\vee A\in \left\{\mathrm{+\infty }\right\}\right)$$
4		pnfex	$$⊢\mathrm{+\infty }\in \mathrm{V}$$
5	4	elsn2	$$⊢A\in \left\{\mathrm{+\infty }\right\}\leftrightarrow A=\mathrm{+\infty }$$
6	5	orbi2i	$$⊢\left(A\in {\mathbb{N}}_0\vee A\in \left\{\mathrm{+\infty }\right\}\right)\leftrightarrow \left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)$$
7	2 3 6	3bitri	$$⊢A\in {\mathbb{N}}_0^{*}\leftrightarrow \left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)$$