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	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ^* , < ) ≠ -∞ )

Proof

Step	Hyp	Ref	Expression
1		mnfxr	⊢ -∞ ∈ ℝ^*
2	1	a1i	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴 ) → -∞ ∈ ℝ^* )
3		supxrcl	⊢ ( 𝐴 ⊆ ℝ^* → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
4	3	3ad2ant1	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
5		simp1	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴 ) → 𝐴 ⊆ ℝ^* )
6	5 1	jctir	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴 ) → ( 𝐴 ⊆ ℝ^* ∧ -∞ ∈ ℝ^* ) )
7		simpl	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ ¬ -∞ ∈ 𝐴 ) → 𝐴 ⊆ ℝ^* )
8	7	sselda	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ ¬ -∞ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ^* )
9		simpr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ ¬ -∞ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
10		simplr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ ¬ -∞ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ -∞ ∈ 𝐴 )
11		nelneq	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ -∞ ∈ 𝐴 ) → ¬ 𝑥 = -∞ )
12	9 10 11	syl2anc	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ ¬ -∞ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 = -∞ )
13		ngtmnft	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑥 = -∞ ↔ ¬ -∞ < 𝑥 ) )
14	13	biimprd	⊢ ( 𝑥 ∈ ℝ^* → ( ¬ -∞ < 𝑥 → 𝑥 = -∞ ) )
15	14	con1d	⊢ ( 𝑥 ∈ ℝ^* → ( ¬ 𝑥 = -∞ → -∞ < 𝑥 ) )
16	8 12 15	sylc	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ ¬ -∞ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → -∞ < 𝑥 )
17	16	reximdva0	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ ¬ -∞ ∈ 𝐴 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 -∞ < 𝑥 )
18	17	3impa	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ ¬ -∞ ∈ 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 -∞ < 𝑥 )
19	18	3com23	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 -∞ < 𝑥 )
20		supxrlub	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ -∞ ∈ ℝ^* ) → ( -∞ < sup ( 𝐴 , ℝ^* , < ) ↔ ∃ 𝑥 ∈ 𝐴 -∞ < 𝑥 ) )
21	20	biimprd	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ -∞ ∈ ℝ^* ) → ( ∃ 𝑥 ∈ 𝐴 -∞ < 𝑥 → -∞ < sup ( 𝐴 , ℝ^* , < ) ) )
22	6 19 21	sylc	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴 ) → -∞ < sup ( 𝐴 , ℝ^* , < ) )
23		xrltne	⊢ ( ( -∞ ∈ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* ∧ -∞ < sup ( 𝐴 , ℝ^* , < ) ) → sup ( 𝐴 , ℝ^* , < ) ≠ -∞ )
24	2 4 22 23	syl3anc	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ^* , < ) ≠ -∞ )

Metamath Proof Explorer

Theorem supxrnemnf

Proof