Metamath Proof Explorer

Theorem suprleubii

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
Hypothesis sup3i.1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
Assertion suprleubii ⊢ B ∈ ℝ → sup A ℝ < ≤ B ↔ ∀ z ∈ A z ≤ B

Proof

Step Hyp Ref Expression
1 sup3i.1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
2 suprleub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → sup A ℝ < ≤ B ↔ ∀ z ∈ A z ≤ B
3 1 2 mpan ⊢ B ∈ ℝ → sup A ℝ < ≤ B ↔ ∀ z ∈ A z ≤ B