Metamath Proof Explorer


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 ∪ { +∞ } )