Metamath Proof Explorer

Theorem supicclub

Description: The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019)

Ref Expression
Hypotheses supicc.1 ⊢ φ → B ∈ ℝ
supicc.2 ⊢ φ → C ∈ ℝ
supicc.3 ⊢ φ → A ⊆ B C
supicc.4 ⊢ φ → A ≠ ∅
supiccub.1 ⊢ φ → D ∈ A
Assertion supicclub ⊢ φ → D < sup A ℝ < ↔ ∃ z ∈ A D < z

Proof

Step Hyp Ref Expression
1 supicc.1 ⊢ φ → B ∈ ℝ
2 supicc.2 ⊢ φ → C ∈ ℝ
3 supicc.3 ⊢ φ → A ⊆ B C
4 supicc.4 ⊢ φ → A ≠ ∅
5 supiccub.1 ⊢ φ → D ∈ A
6 iccssre ⊢ B ∈ ℝ ∧ C ∈ ℝ → B C ⊆ ℝ
7 1 2 6 syl2anc ⊢ φ → B C ⊆ ℝ
8 3 7 sstrd ⊢ φ → A ⊆ ℝ
9 1 adantr ⊢ φ ∧ x ∈ A → B ∈ ℝ
10 9 rexrd ⊢ φ ∧ x ∈ A → B ∈ ℝ *
11 2 adantr ⊢ φ ∧ x ∈ A → C ∈ ℝ
12 11 rexrd ⊢ φ ∧ x ∈ A → C ∈ ℝ *
13 3 sselda ⊢ φ ∧ x ∈ A → x ∈ B C
14 iccleub ⊢ B ∈ ℝ * ∧ C ∈ ℝ * ∧ x ∈ B C → x ≤ C
15 10 12 13 14 syl3anc ⊢ φ ∧ x ∈ A → x ≤ C
16 15 ralrimiva ⊢ φ → ∀ x ∈ A x ≤ C
17 brralrspcev ⊢ C ∈ ℝ ∧ ∀ x ∈ A x ≤ C → ∃ y ∈ ℝ ∀ x ∈ A x ≤ y
18 2 16 17 syl2anc ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A x ≤ y
19 8 5 sseldd ⊢ φ → D ∈ ℝ
20 suprlub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ y ∈ ℝ ∀ x ∈ A x ≤ y ∧ D ∈ ℝ → D < sup A ℝ < ↔ ∃ z ∈ A D < z
21 8 4 18 19 20 syl31anc ⊢ φ → D < sup A ℝ < ↔ ∃ z ∈ A D < z