Theorem supicc

Description: Supremum of a bounded set of real numbers. (Contributed by Thierry Arnoux, 17-May-2019)

	Ref	Expression
Hypotheses	supicc.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	supicc.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	supicc.3	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐵 [,] 𝐶 ) )
	supicc.4	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion	supicc	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ( 𝐵 [,] 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		supicc.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2		supicc.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3		supicc.3	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐵 [,] 𝐶 ) )
4		supicc.4	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5		iccssre	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 [,] 𝐶 ) ⊆ ℝ )
6	1 2 5	syl2anc	⊢ ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ℝ )
7	3 6	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
9	8	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
11	10	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
12	3	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝐵 [,] 𝐶 ) )
13		iccleub	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝑥 ≤ 𝐶 )
14	9 11 12 13	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ 𝐶 )
15	14	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐶 )
16		brralrspcev	⊢ ( ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐶 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 )
17	2 15 16	syl2anc	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 )
18		suprcl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
19	7 4 17 18	syl3anc	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
20	7	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
21	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ( 𝐵 [,] 𝐶 ) )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
23		iccsupr	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 ⊆ ( 𝐵 [,] 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
24	8 10 21 22 23	syl211anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
25	24 18	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
26		iccgelb	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝐵 ≤ 𝑥 )
27	9 11 12 26	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑥 )
28		suprub	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ , < ) )
29	24 22 28	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ , < ) )
30	8 20 25 27 29	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )
31	30	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )
32		r19.3rzv	⊢ ( 𝐴 ≠ ∅ → ( 𝐵 ≤ sup ( 𝐴 , ℝ , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ sup ( 𝐴 , ℝ , < ) ) )
33	4 32	syl	⊢ ( 𝜑 → ( 𝐵 ≤ sup ( 𝐴 , ℝ , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ sup ( 𝐴 , ℝ , < ) ) )
34	31 33	mpbird	⊢ ( 𝜑 → 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )
35		suprleub	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐶 ∈ ℝ ) → ( sup ( 𝐴 , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐶 ) )
36	7 4 17 2 35	syl31anc	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐶 ) )
37	15 36	mpbird	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ≤ 𝐶 )
38		elicc2	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( sup ( 𝐴 , ℝ , < ) ∈ ( 𝐵 [,] 𝐶 ) ↔ ( sup ( 𝐴 , ℝ , < ) ∈ ℝ ∧ 𝐵 ≤ sup ( 𝐴 , ℝ , < ) ∧ sup ( 𝐴 , ℝ , < ) ≤ 𝐶 ) ) )
39	1 2 38	syl2anc	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) ∈ ( 𝐵 [,] 𝐶 ) ↔ ( sup ( 𝐴 , ℝ , < ) ∈ ℝ ∧ 𝐵 ≤ sup ( 𝐴 , ℝ , < ) ∧ sup ( 𝐴 , ℝ , < ) ≤ 𝐶 ) ) )
40	19 34 37 39	mpbir3and	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ( 𝐵 [,] 𝐶 ) )