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

Metamath Proof Explorer

Theorem supxrre3

Description: The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion supxrre3 ⊢ A ⊆ ℝ ∧ A ≠ ∅ → sup A ℝ * < ∈ ℝ ↔ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x

Proof

Step Hyp Ref Expression
1 supxrre1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ → sup A ℝ * < ∈ ℝ ↔ sup A ℝ * < < +∞
2 id ⊢ A ⊆ ℝ → A ⊆ ℝ
3 rexr ⊢ x ∈ ℝ → x ∈ ℝ *
4 3 ssriv ⊢ ℝ ⊆ ℝ *
5 4 a1i ⊢ A ⊆ ℝ → ℝ ⊆ ℝ *
6 2 5 sstrd ⊢ A ⊆ ℝ → A ⊆ ℝ *
7 supxrbnd2 ⊢ A ⊆ ℝ * → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ↔ sup A ℝ * < < +∞
8 6 7 syl ⊢ A ⊆ ℝ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ↔ sup A ℝ * < < +∞
9 8 bicomd ⊢ A ⊆ ℝ → sup A ℝ * < < +∞ ↔ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
10 9 adantr ⊢ A ⊆ ℝ ∧ A ≠ ∅ → sup A ℝ * < < +∞ ↔ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
11 1 10 bitrd ⊢ A ⊆ ℝ ∧ A ≠ ∅ → sup A ℝ * < ∈ ℝ ↔ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x