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 ( ℝ* , ℝ* , < ) = +∞