Definition df-xnn0

Description: Define the set of extended nonnegative integers that includes positive infinity. Analogue of the extension of the real numbers RR* , see df-xr . (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	df-xnn0	$$⊢{\mathbb{N}}_0^{*}={\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxnn0	$$class{\mathbb{N}}_0^{*}$$
1		cn0	$$class{\mathbb{N}}_0$$
2		cpnf	$$class\mathrm{+\infty }$$
3	2	csn	$$class\left\{\mathrm{+\infty }\right\}$$
4	1 3	cun	$$class\left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)$$
5	0 4	wceq	$$wff{\mathbb{N}}_0^{*}={\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$