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

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 ( ( 𝐴 ⊆ ℝ ∧ 𝑈 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑈 ) → 𝑈 = sup ( 𝐴 , ℝ , < ) )

Proof

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