Metamath Proof Explorer

Theorem supxr2

Description: The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006)

Ref Expression
Assertion supxr2 ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ A x ≤ B ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → sup A ℝ * < = B

Proof

Step Hyp Ref Expression
1 ssel2 ⊢ A ⊆ ℝ * ∧ x ∈ A → x ∈ ℝ *
2 xrlenlt ⊢ x ∈ ℝ * ∧ B ∈ ℝ * → x ≤ B ↔ ¬ B < x
3 1 2 sylan ⊢ A ⊆ ℝ * ∧ x ∈ A ∧ B ∈ ℝ * → x ≤ B ↔ ¬ B < x
4 3 an32s ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ x ∈ A → x ≤ B ↔ ¬ B < x
5 4 ralbidva ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ∀ x ∈ A x ≤ B ↔ ∀ x ∈ A ¬ B < x
6 5 anbi1d ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ∀ x ∈ A x ≤ B ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y ↔ ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y
7 6 biimpa ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ A x ≤ B ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y
8 supxr ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → sup A ℝ * < = B
9 7 8 syldan ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ A x ≤ B ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → sup A ℝ * < = B