Metamath Proof Explorer

Theorem supicc

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

Ref Expression
Hypotheses supicc.1 ⊢φ→B∈ℝ
supicc.2 ⊢φ→C∈ℝ
supicc.3 ⊢φ→A⊆BC
supicc.4 ⊢φ→A≠∅
Assertion supicc ⊢φ→supAℝ<∈BC

Proof

Step Hyp Ref Expression
1 supicc.1 ⊢φ→B∈ℝ
2 supicc.2 ⊢φ→C∈ℝ
3 supicc.3 ⊢φ→A⊆BC
4 supicc.4 ⊢φ→A≠∅
5 iccssre ⊢B∈ℝ∧C∈ℝ→BC⊆ℝ
6 1 2 5 syl2anc ⊢φ→BC⊆ℝ
7 3 6 sstrd ⊢φ→A⊆ℝ
8 1 adantr ⊢φ∧x∈A→B∈ℝ
9 8 rexrd ⊢φ∧x∈A→B∈ℝ*
10 2 adantr ⊢φ∧x∈A→C∈ℝ
11 10 rexrd ⊢φ∧x∈A→C∈ℝ*
12 3 sselda ⊢φ∧x∈A→x∈BC
13 iccleub ⊢B∈ℝ*∧C∈ℝ*∧x∈BC→x≤C
14 9 11 12 13 syl3anc ⊢φ∧x∈A→x≤C
15 14 ralrimiva ⊢φ→∀x∈Ax≤C
16 brralrspcev ⊢C∈ℝ∧∀x∈Ax≤C→∃y∈ℝ∀x∈Ax≤y
17 2 15 16 syl2anc ⊢φ→∃y∈ℝ∀x∈Ax≤y
18 suprcl ⊢A⊆ℝ∧A≠∅∧∃y∈ℝ∀x∈Ax≤y→supAℝ<∈ℝ
19 7 4 17 18 syl3anc ⊢φ→supAℝ<∈ℝ
20 7 sselda ⊢φ∧x∈A→x∈ℝ
21 3 adantr ⊢φ∧x∈A→A⊆BC
22 simpr ⊢φ∧x∈A→x∈A
23 iccsupr ⊢B∈ℝ∧C∈ℝ∧A⊆BC∧x∈A→A⊆ℝ∧A≠∅∧∃y∈ℝ∀x∈Ax≤y
24 8 10 21 22 23 syl211anc ⊢φ∧x∈A→A⊆ℝ∧A≠∅∧∃y∈ℝ∀x∈Ax≤y
25 24 18 syl ⊢φ∧x∈A→supAℝ<∈ℝ
26 iccgelb ⊢B∈ℝ*∧C∈ℝ*∧x∈BC→B≤x
27 9 11 12 26 syl3anc ⊢φ∧x∈A→B≤x
28 suprub ⊢A⊆ℝ∧A≠∅∧∃y∈ℝ∀x∈Ax≤y∧x∈A→x≤supAℝ<
29 24 22 28 syl2anc ⊢φ∧x∈A→x≤supAℝ<
30 8 20 25 27 29 letrd ⊢φ∧x∈A→B≤supAℝ<
31 30 ralrimiva ⊢φ→∀x∈AB≤supAℝ<
32 r19.3rzv ⊢A≠∅→B≤supAℝ<↔∀x∈AB≤supAℝ<
33 4 32 syl ⊢φ→B≤supAℝ<↔∀x∈AB≤supAℝ<
34 31 33 mpbird ⊢φ→B≤supAℝ<
35 suprleub ⊢A⊆ℝ∧A≠∅∧∃y∈ℝ∀x∈Ax≤y∧C∈ℝ→supAℝ<≤C↔∀x∈Ax≤C
36 7 4 17 2 35 syl31anc ⊢φ→supAℝ<≤C↔∀x∈Ax≤C
37 15 36 mpbird ⊢φ→supAℝ<≤C
38 elicc2 ⊢B∈ℝ∧C∈ℝ→supAℝ<∈BC↔supAℝ<∈ℝ∧B≤supAℝ<∧supAℝ<≤C
39 1 2 38 syl2anc ⊢φ→supAℝ<∈BC↔supAℝ<∈ℝ∧B≤supAℝ<∧supAℝ<≤C
40 19 34 37 39 mpbir3and ⊢φ→supAℝ<∈BC