Theorem rpsup

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

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

Proof

Step	Hyp	Ref	Expression
1		ioorp	⊢ ( 0 (,) +∞ ) = ℝ+
2	1	supeq1i	⊢ sup ( ( 0 (,) +∞ ) , ℝ* , < ) = sup ( ℝ+ , ℝ* , < )
3		0xr	⊢ 0 ∈ ℝ*
4		0re	⊢ 0 ∈ ℝ
5		renepnf	⊢ ( 0 ∈ ℝ → 0 ≠ +∞ )
6	4 5	ax-mp	⊢ 0 ≠ +∞
7		ioopnfsup	⊢ ( ( 0 ∈ ℝ* ∧ 0 ≠ +∞ ) → sup ( ( 0 (,) +∞ ) , ℝ* , < ) = +∞ )
8	3 6 7	mp2an	⊢ sup ( ( 0 (,) +∞ ) , ℝ* , < ) = +∞
9	2 8	eqtr3i	⊢ sup ( ℝ+ , ℝ* , < ) = +∞