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

Metamath Proof Explorer

Theorem suprnub

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

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

Proof

Step Hyp Ref Expression
1 suprlub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → B < sup A ℝ < ↔ ∃ z ∈ A B < z
2 1 notbid ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → ¬ B < sup A ℝ < ↔ ¬ ∃ z ∈ A B < z
3 ralnex ⊢ ∀ z ∈ A ¬ B < z ↔ ¬ ∃ z ∈ A B < z
4 2 3 bitr4di ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → ¬ B < sup A ℝ < ↔ ∀ z ∈ A ¬ B < z