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

Metamath Proof Explorer

Theorem supxrre1

Description: The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006)

Ref Expression
Assertion supxrre1 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )

Proof

Step Hyp Ref Expression
1 supxrgtmnf ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → -∞ < sup ( 𝐴 , ℝ* , < ) )
2 ressxr ⊢ ℝ ⊆ ℝ*
3 sstr ⊢ ( ( 𝐴 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
4 2 3 mpan2 ⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ* )
5 supxrcl ⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
6 xrrebnd ⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
7 4 5 6 3syl ⊢ ( 𝐴 ⊆ ℝ → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
8 7 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
9 1 8 mpbirand ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )