Theorem resup

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

	Ref	Expression
Assertion	resup	⊢ sup ( ℝ , ℝ* , < ) = +∞

Proof

Step	Hyp	Ref	Expression
1		ioomax	⊢ ( -∞ (,) +∞ ) = ℝ
2	1	supeq1i	⊢ sup ( ( -∞ (,) +∞ ) , ℝ* , < ) = sup ( ℝ , ℝ* , < )
3		mnfxr	⊢ -∞ ∈ ℝ*
4		mnfnepnf	⊢ -∞ ≠ +∞
5		ioopnfsup	⊢ ( ( -∞ ∈ ℝ* ∧ -∞ ≠ +∞ ) → sup ( ( -∞ (,) +∞ ) , ℝ* , < ) = +∞ )
6	3 4 5	mp2an	⊢ sup ( ( -∞ (,) +∞ ) , ℝ* , < ) = +∞
7	2 6	eqtr3i	⊢ sup ( ℝ , ℝ* , < ) = +∞