supxrre2

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

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

Step	Hyp	Ref	Expression
1		supxrre1	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow 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		nltpnft	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
7	4 5 6	3syl	$⊢ A \subseteq ℝ \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
8	7	necon2abid	$⊢ A \subseteq ℝ \to (sup (A ℝ^{} <) < +∞ \leftrightarrow sup (A ℝ^{} <) \neq +∞)$
9	8	adantr	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) < +∞ \leftrightarrow sup (A ℝ^{} <) \neq +∞)$
10	1 9	bitrd	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow sup (A ℝ^{} <) \neq +∞)$

Metamath Proof Explorer