Metamath Proof Explorer

Theorem supxr

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

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

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → B ∈ ℝ *
2 simprl ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → ∀ x ∈ A ¬ B < x
3 xrub ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * → ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y ↔ ∀ x ∈ ℝ * x < B → ∃ y ∈ A x < y
4 3 biimpa ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → ∀ x ∈ ℝ * x < B → ∃ y ∈ A x < y
5 4 adantrl ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → ∀ x ∈ ℝ * x < B → ∃ y ∈ A x < y
6 xrltso ⊢ < Or ℝ *
7 6 a1i ⊢ ⊤ → < Or ℝ *
8 7 eqsup ⊢ ⊤ → B ∈ ℝ * ∧ ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ * x < B → ∃ y ∈ A x < y → sup A ℝ * < = B
9 8 mptru ⊢ B ∈ ℝ * ∧ ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ * x < B → ∃ y ∈ A x < y → sup A ℝ * < = B
10 1 2 5 9 syl3anc ⊢ A ⊆ ℝ * ∧ B ∈ ℝ * ∧ ∀ x ∈ A ¬ B < x ∧ ∀ x ∈ ℝ x < B → ∃ y ∈ A x < y → sup A ℝ * < = B