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	|- NN0* = ( NN0 u. { +oo } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxnn0	|- NN0*
1		cn0	|- NN0
2		cpnf	|- +oo
3	2	csn	|- { +oo }
4	1 3	cun	|- ( NN0 u. { +oo } )
5	0 4	wceq	|- NN0* = ( NN0 u. { +oo } )