Metamath Proof Explorer

Theorem xrsup

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

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

Proof

Step Hyp Ref Expression
1 ssid 
 |-  RR* C_ RR*
2 pnfxr 
 |-  +oo e. RR*
3 supxrpnf 
 |-  ( ( RR* C_ RR* /\ +oo e. RR* ) -> sup ( RR* , RR* , < ) = +oo )
4 1 2 3 mp2an 
 |-  sup ( RR* , RR* , < ) = +oo