supxrgtmnf

Description: The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006)

		Ref	Expression
	Assertion	supxrgtmnf	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to −∞ < sup (A ℝ^{*} <)$

Step	Hyp	Ref	Expression
1		supxrbnd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land sup (A ℝ^{} <) < +∞) \to sup (A ℝ^{} <) \in ℝ$
2	1	3expia	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) < +∞ \to sup (A ℝ^{} <) \in ℝ)$
3	2	con3d	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (\neg sup (A ℝ^{} <) \in ℝ \to \neg sup (A ℝ^{} <) < +∞)$
4		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
5		sstr	$⊢ (A \subseteq ℝ \land ℝ \subseteq ℝ^{}) \to A \subseteq ℝ^{}$
6	4 5	mpan2	$⊢ A \subseteq ℝ \to A \subseteq ℝ^{*}$
7		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
8	6 7	syl	$⊢ A \subseteq ℝ \to sup (A ℝ^{} <) \in ℝ^{}$
9	8	adantr	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to sup (A ℝ^{} <) \in ℝ^{}$
10		nltpnft	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
11	9 10	syl	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
12	3 11	sylibrd	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (\neg sup (A ℝ^{} <) \in ℝ \to sup (A ℝ^{} <) = +∞)$
13	12	orrd	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (sup (A ℝ^{} <) \in ℝ \lor sup (A ℝ^{} <) = +∞)$
14		mnfltxr	$⊢ (sup (A ℝ^{} <) \in ℝ \lor sup (A ℝ^{} <) = +∞) \to −∞ < sup (A ℝ^{*} <)$
15	13 14	syl	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to −∞ < sup (A ℝ^{*} <)$

Metamath Proof Explorer