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 ( 𝐴 , ℝ , < ) )