Metamath Proof Explorer

Theorem resup

Description: The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016)

Ref Expression
Assertion resup 
|- sup ( RR , RR* , < ) = +oo

Proof

Step Hyp Ref Expression
1 ioomax 
 |-  ( -oo (,) +oo ) = RR
2 1 supeq1i 
 |-  sup ( ( -oo (,) +oo ) , RR* , < ) = sup ( RR , RR* , < )
3 mnfxr 
 |-  -oo e. RR*
4 mnfnepnf 
 |-  -oo =/= +oo
5 ioopnfsup 
 |-  ( ( -oo e. RR* /\ -oo =/= +oo ) -> sup ( ( -oo (,) +oo ) , RR* , < ) = +oo )
6 3 4 5 mp2an 
 |-  sup ( ( -oo (,) +oo ) , RR* , < ) = +oo
7 2 6 eqtr3i 
 |-  sup ( RR , RR* , < ) = +oo