Theorem 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 ( 𝐴 , ℝ* , < ) ≠ -∞ )