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

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 (ℝ^{} ℝ^{} <) = +∞$

Step	Hyp	Ref	Expression
1		ssid	$⊢ ℝ^{} \subseteq ℝ^{}$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3		supxrpnf	$⊢ (ℝ^{} \subseteq ℝ^{} \land +∞ \in ℝ^{}) \to sup (ℝ^{} ℝ^{*} <) = +∞$
4	1 2 3	mp2an	$⊢ sup (ℝ^{} ℝ^{} <) = +∞$