This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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