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

Metamath Proof Explorer

Theorem suprleub

Description: The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 6-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 suprnub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → ¬ B < sup A ℝ < ↔ ∀ w ∈ A ¬ B < w
2 suprcl ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → sup A ℝ < ∈ ℝ
3 lenlt ⊢ sup A ℝ < ∈ ℝ ∧ B ∈ ℝ → sup A ℝ < ≤ B ↔ ¬ B < sup A ℝ <
4 2 3 sylan ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → sup A ℝ < ≤ B ↔ ¬ B < sup A ℝ <
5 simpl1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → A ⊆ ℝ
6 5 sselda ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ ∧ w ∈ A → w ∈ ℝ
7 simplr ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ ∧ w ∈ A → B ∈ ℝ
8 6 7 lenltd ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ ∧ w ∈ A → w ≤ B ↔ ¬ B < w
9 8 ralbidva ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → ∀ w ∈ A w ≤ B ↔ ∀ w ∈ A ¬ B < w
10 1 4 9 3bitr4d ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → sup A ℝ < ≤ B ↔ ∀ w ∈ A w ≤ B
11 breq1 ⊢ w = z → w ≤ B ↔ z ≤ B
12 11 cbvralvw ⊢ ∀ w ∈ A w ≤ B ↔ ∀ z ∈ A z ≤ B
13 10 12 bitrdi ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → sup A ℝ < ≤ B ↔ ∀ z ∈ A z ≤ B