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

Metamath Proof Explorer

Theorem suprlub

Description: The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 6-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 ltso ⊢ < Or ℝ
2 1 a1i ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → < Or ℝ
3 sup3 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → ∃ x ∈ ℝ ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ w ∈ A y < w
4 simp1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → A ⊆ ℝ
5 2 3 4 suplub2 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → B < sup A ℝ < ↔ ∃ w ∈ A B < w
6 breq2 ⊢ w = z → B < w ↔ B < z
7 6 cbvrexvw ⊢ ∃ w ∈ A B < w ↔ ∃ z ∈ A B < z
8 5 7 bitrdi ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → B < sup A ℝ < ↔ ∃ z ∈ A B < z