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	⊢ ℕ0* = ( ℕ0 ∪ { +∞ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxnn0	⊢ ℕ0*
1		cn0	⊢ ℕ0
2		cpnf	⊢ +∞
3	2	csn	⊢ { +∞ }
4	1 3	cun	⊢ ( ℕ0 ∪ { +∞ } )
5	0 4	wceq	⊢ ℕ0* = ( ℕ0 ∪ { +∞ } )