Description: An extended nonnegative integer is either a standard nonnegative integer or positive infinity. (Contributed by AV, 10-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | elxnn0 | |- ( A e. NN0* <-> ( A e. NN0 \/ A = +oo ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xnn0 | |- NN0* = ( NN0 u. { +oo } ) |
|
2 | 1 | eleq2i | |- ( A e. NN0* <-> A e. ( NN0 u. { +oo } ) ) |
3 | elun | |- ( A e. ( NN0 u. { +oo } ) <-> ( A e. NN0 \/ A e. { +oo } ) ) |
|
4 | pnfex | |- +oo e. _V |
|
5 | 4 | elsn2 | |- ( A e. { +oo } <-> A = +oo ) |
6 | 5 | orbi2i | |- ( ( A e. NN0 \/ A e. { +oo } ) <-> ( A e. NN0 \/ A = +oo ) ) |
7 | 2 3 6 | 3bitri | |- ( A e. NN0* <-> ( A e. NN0 \/ A = +oo ) ) |