Metamath Proof Explorer

Theorem nn0nepnf

Description: No standard nonnegative integer equals positive infinity. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion nn0nepnf 
|- ( A e. NN0 -> A =/= +oo )

Proof

Step Hyp Ref Expression
1 pnfnre 
 |-  +oo e/ RR
2 1 neli 
 |-  -. +oo e. RR
3 nn0re 
 |-  ( +oo e. NN0 -> +oo e. RR )
4 2 3 mto 
 |-  -. +oo e. NN0
5 eleq1 
 |-  ( A = +oo -> ( A e. NN0 <-> +oo e. NN0 ) )
6 4 5 mtbiri 
 |-  ( A = +oo -> -. A e. NN0 )
7 6 necon2ai 
 |-  ( A e. NN0 -> A =/= +oo )