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