Metamath Proof Explorer

Theorem ubelsupr

Description: If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Assertion ubelsupr ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → U = sup A ℝ <

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → A ⊆ ℝ
2 simp2 ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → U ∈ A
3 2 ne0d ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → A ≠ ∅
4 1 2 sseldd ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → U ∈ ℝ
5 simp3 ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → ∀ x ∈ A x ≤ U
6 brralrspcev ⊢ U ∈ ℝ ∧ ∀ x ∈ A x ≤ U → ∃ y ∈ ℝ ∀ x ∈ A x ≤ y
7 4 5 6 syl2anc ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → ∃ y ∈ ℝ ∀ x ∈ A x ≤ y
8 1 3 7 3jca ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ y ∈ ℝ ∀ x ∈ A x ≤ y
9 suprub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ y ∈ ℝ ∀ x ∈ A x ≤ y ∧ U ∈ A → U ≤ sup A ℝ <
10 8 2 9 syl2anc ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → U ≤ sup A ℝ <
11 suprleub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ y ∈ ℝ ∀ x ∈ A x ≤ y ∧ U ∈ ℝ → sup A ℝ < ≤ U ↔ ∀ x ∈ A x ≤ U
12 8 4 11 syl2anc ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → sup A ℝ < ≤ U ↔ ∀ x ∈ A x ≤ U
13 5 12 mpbird ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → sup A ℝ < ≤ U
14 suprcl ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ y ∈ ℝ ∀ x ∈ A x ≤ y → sup A ℝ < ∈ ℝ
15 8 14 syl ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → sup A ℝ < ∈ ℝ
16 4 15 letri3d ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → U = sup A ℝ < ↔ U ≤ sup A ℝ < ∧ sup A ℝ < ≤ U
17 10 13 16 mpbir2and ⊢ A ⊆ ℝ ∧ U ∈ A ∧ ∀ x ∈ A x ≤ U → U = sup A ℝ <