Metamath Proof Explorer

Theorem xnn0nnn0pnf

Description: An extended nonnegative integer which is not a standard nonnegative integer is positive infinity. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion xnn0nnn0pnf 
|- ( ( N e. NN0* /\ -. N e. NN0 ) -> N = +oo )

Proof

Step Hyp Ref Expression
1 elxnn0 
 |-  ( N e. NN0* <-> ( N e. NN0 \/ N = +oo ) )
2 pm2.53 
 |-  ( ( N e. NN0 \/ N = +oo ) -> ( -. N e. NN0 -> N = +oo ) )
3 1 2 sylbi 
 |-  ( N e. NN0* -> ( -. N e. NN0 -> N = +oo ) )
4 3 imp 
 |-  ( ( N e. NN0* /\ -. N e. NN0 ) -> N = +oo )