This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpsup

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

		Ref	Expression
	Assertion	rpsup	$⊢ sup (ℝ^{+} ℝ^{*} <) = +∞$

Step	Hyp	Ref	Expression
1		ioorp	$⊢ (0, +∞) = ℝ^{+}$
2	1	supeq1i	$⊢ sup ((0, +∞) ℝ^{} <) = sup (ℝ^{+} ℝ^{} <)$
3		0xr	$⊢ 0 \in ℝ^{*}$
4		0re	$⊢ 0 \in ℝ$
5		renepnf	$⊢ 0 \in ℝ \to 0 \neq +∞$
6	4 5	ax-mp	$⊢ 0 \neq +∞$
7		ioopnfsup	$⊢ (0 \in ℝ^{} \land 0 \neq +∞) \to sup ((0, +∞) ℝ^{} <) = +∞$
8	3 6 7	mp2an	$⊢ sup ((0, +∞) ℝ^{*} <) = +∞$
9	2 8	eqtr3i	$⊢ sup (ℝ^{+} ℝ^{*} <) = +∞$