supxrre1

Description: The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006)

		Ref	Expression
	Assertion	supxrre1	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow sup (A ℝ^{} <) < +∞)$

Step	Hyp	Ref	Expression
1		supxrgtmnf	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to −∞ < sup (A ℝ^{*} <)$
2		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
3		sstr	$⊢ (A \subseteq ℝ \land ℝ \subseteq ℝ^{}) \to A \subseteq ℝ^{}$
4	2 3	mpan2	$⊢ A \subseteq ℝ \to A \subseteq ℝ^{*}$
5		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
6		xrrebnd	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞))$
7	4 5 6	3syl	$⊢ A \subseteq ℝ \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞))$
8	7	adantr	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞))$
9	1 8	mpbirand	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow sup (A ℝ^{} <) < +∞)$

Metamath Proof Explorer