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 class0*
1 cn0 class0
2 cpnf class+∞
3 2 csn class+∞
4 1 3 cun class0+∞
5 0 4 wceq wff0*=0+∞