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

Metamath Proof Explorer

Theorem resup

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

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

Step	Hyp	Ref	Expression
1		ioomax	$⊢ (−∞, +∞) = ℝ$
2	1	supeq1i	$⊢ sup ((−∞, +∞) ℝ^{} <) = sup (ℝ ℝ^{} <)$
3		mnfxr	$⊢ −∞ \in ℝ^{*}$
4		mnfnepnf	$⊢ −∞ \neq +∞$
5		ioopnfsup	$⊢ (−∞ \in ℝ^{} \land −∞ \neq +∞) \to sup ((−∞, +∞) ℝ^{} <) = +∞$
6	3 4 5	mp2an	$⊢ sup ((−∞, +∞) ℝ^{*} <) = +∞$
7	2 6	eqtr3i	$⊢ sup (ℝ ℝ^{*} <) = +∞$