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

Metamath Proof Explorer

Theorem supxrre2

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

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

Proof

Step Hyp Ref Expression
1 supxrre1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
2 ressxr ⊢ ℝ ⊆ ℝ*
3 sstr ⊢ ( ( 𝐴 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
4 2 3 mpan2 ⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ* )
5 supxrcl ⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
6 nltpnft ⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
7 4 5 6 3syl ⊢ ( 𝐴 ⊆ ℝ → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
8 7 necon2abid ⊢ ( 𝐴 ⊆ ℝ → ( sup ( 𝐴 , ℝ* , < ) < +∞ ↔ sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
9 8 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) < +∞ ↔ sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
10 1 9 bitrd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )