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

Metamath Proof Explorer

Theorem supxrleub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion supxrleub ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → sup A ℝ * < ≤ B ↔ ∀ x ∈ A x ≤ B

Proof

Step Hyp Ref Expression
1 supxrlub ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → B < sup A ℝ * < ↔ ∃ x ∈ A B < x
2 1 notbid ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ¬ B < sup A ℝ * < ↔ ¬ ∃ x ∈ A B < x
3 ralnex ⊢ ∀ x ∈ A ¬ B < x ↔ ¬ ∃ x ∈ A B < x
4 2 3 bitr4di ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ¬ B < sup A ℝ * < ↔ ∀ x ∈ A ¬ B < x
5 supxrcl ⊢ A ⊆ ℝ * → sup A ℝ * < ∈ ℝ *
6 xrlenlt ⊢ sup A ℝ * < ∈ ℝ * ∧ B ∈ ℝ * → sup A ℝ * < ≤ B ↔ ¬ B < sup A ℝ * <
7 5 6 sylan ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → sup A ℝ * < ≤ B ↔ ¬ B < sup A ℝ * <
8 simpl ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → A ⊆ ℝ *
9 8 sselda ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ x ∈ A → x ∈ ℝ *
10 simplr ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ x ∈ A → B ∈ ℝ *
11 9 10 xrlenltd ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ x ∈ A → x ≤ B ↔ ¬ B < x
12 11 ralbidva ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ∀ x ∈ A x ≤ B ↔ ∀ x ∈ A ¬ B < x
13 4 7 12 3bitr4d ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → sup A ℝ * < ≤ B ↔ ∀ x ∈ A x ≤ B