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 * * < = +∞

Proof

Step Hyp Ref Expression
1 ssid * *
2 pnfxr +∞ *
3 supxrpnf * * +∞ * sup * * < = +∞
4 1 2 3 mp2an sup * * < = +∞