supxrnemnf

Description: The supremum of a nonempty set of extended reals which does not contain minus infinity is not minus infinity. (Contributed by Thierry Arnoux, 21-Mar-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mnfxr	$⊢ −∞ \in ℝ^{*}$
2	1	a1i	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset \land \neg −∞ \in A) \to −∞ \in ℝ^{}$
3		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
4	3	3ad2ant1	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset \land \neg −∞ \in A) \to sup (A ℝ^{} <) \in ℝ^{*}$
5		simp1	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset \land \neg −∞ \in A) \to A \subseteq ℝ^{}$
6	5 1	jctir	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset \land \neg −∞ \in A) \to (A \subseteq ℝ^{} \land −∞ \in ℝ^{*})$
7		simpl	$⊢ (A \subseteq ℝ^{} \land \neg −∞ \in A) \to A \subseteq ℝ^{}$
8	7	sselda	$⊢ ((A \subseteq ℝ^{} \land \neg −∞ \in A) \land x \in A) \to x \in ℝ^{}$
9		simpr	$⊢ ((A \subseteq ℝ^{*} \land \neg −∞ \in A) \land x \in A) \to x \in A$
10		simplr	$⊢ ((A \subseteq ℝ^{*} \land \neg −∞ \in A) \land x \in A) \to \neg −∞ \in A$
11		nelneq	$⊢ (x \in A \land \neg −∞ \in A) \to \neg x = −∞$
12	9 10 11	syl2anc	$⊢ ((A \subseteq ℝ^{*} \land \neg −∞ \in A) \land x \in A) \to \neg x = −∞$
13		ngtmnft	$⊢ x \in ℝ^{*} \to (x = −∞ \leftrightarrow \neg −∞ < x)$
14	13	biimprd	$⊢ x \in ℝ^{*} \to (\neg −∞ < x \to x = −∞)$
15	14	con1d	$⊢ x \in ℝ^{*} \to (\neg x = −∞ \to −∞ < x)$
16	8 12 15	sylc	$⊢ ((A \subseteq ℝ^{*} \land \neg −∞ \in A) \land x \in A) \to −∞ < x$
17	16	reximdva0	$⊢ ((A \subseteq ℝ^{*} \land \neg −∞ \in A) \land A \neq \emptyset) \to \exists x \in A −∞ < x$
18	17	3impa	$⊢ (A \subseteq ℝ^{*} \land \neg −∞ \in A \land A \neq \emptyset) \to \exists x \in A −∞ < x$
19	18	3com23	$⊢ (A \subseteq ℝ^{*} \land A \neq \emptyset \land \neg −∞ \in A) \to \exists x \in A −∞ < x$
20		supxrlub	$⊢ (A \subseteq ℝ^{} \land −∞ \in ℝ^{}) \to (−∞ < sup (A ℝ^{*} <) \leftrightarrow \exists x \in A −∞ < x)$
21	20	biimprd	$⊢ (A \subseteq ℝ^{} \land −∞ \in ℝ^{}) \to (\exists x \in A −∞ < x \to −∞ < sup (A ℝ^{*} <))$
22	6 19 21	sylc	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset \land \neg −∞ \in A) \to −∞ < sup (A ℝ^{} <)$
23		xrltne	$⊢ (−∞ \in ℝ^{} \land sup (A ℝ^{} <) \in ℝ^{} \land −∞ < sup (A ℝ^{} <)) \to sup (A ℝ^{*} <) \neq −∞$
24	2 4 22 23	syl3anc	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset \land \neg −∞ \in A) \to sup (A ℝ^{} <) \neq −∞$

Metamath Proof Explorer

Theorem supxrnemnf

Proof