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

Proof

Step	Hyp	Ref	Expression
1		supxrbnd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
2	1	3expia	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) < +∞ → sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) )
3	2	con3d	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ¬ sup ( 𝐴 , ℝ* , < ) ∈ ℝ → ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
4		ressxr	⊢ ℝ ⊆ ℝ*
5		sstr	⊢ ( ( 𝐴 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
6	4 5	mpan2	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ* )
7		supxrcl	⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
8	6 7	syl	⊢ ( 𝐴 ⊆ ℝ → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
9	8	adantr	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
10		nltpnft	⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
11	9 10	syl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
12	3 11	sylibrd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ¬ sup ( 𝐴 , ℝ* , < ) ∈ ℝ → sup ( 𝐴 , ℝ* , < ) = +∞ ) )
13	12	orrd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∨ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
14		mnfltxr	⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∨ sup ( 𝐴 , ℝ* , < ) = +∞ ) → -∞ < sup ( 𝐴 , ℝ* , < ) )
15	13 14	syl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → -∞ < sup ( 𝐴 , ℝ* , < ) )