Metamath Proof Explorer

Theorem pnf0xnn0

Description: Positive infinity is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion pnf0xnn0 
|- +oo e. NN0*

Proof

Step Hyp Ref Expression
1 eqid 
 |-  +oo = +oo
2 1 olci 
 |-  ( +oo e. NN0 \/ +oo = +oo )
3 elxnn0 
 |-  ( +oo e. NN0* <-> ( +oo e. NN0 \/ +oo = +oo ) )
4 2 3 mpbir 
 |-  +oo e. NN0*