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
|- 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 } )