Metamath Proof Explorer

Theorem upbdrech

Description: Choice of an upper bound for a nonempty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses upbdrech.a ⊢φ→A≠∅
upbdrech.b ⊢φ∧x∈A→B∈ℝ
upbdrech.bd ⊢φ→∃y∈ℝ∀x∈AB≤y
upbdrech.c ⊢C=supz|∃x∈Az=Bℝ<
Assertion upbdrech ⊢φ→C∈ℝ∧∀x∈AB≤C

Proof

Step Hyp Ref Expression
1 upbdrech.a ⊢φ→A≠∅
2 upbdrech.b ⊢φ∧x∈A→B∈ℝ
3 upbdrech.bd ⊢φ→∃y∈ℝ∀x∈AB≤y
4 upbdrech.c ⊢C=supz|∃x∈Az=Bℝ<
5 2 ralrimiva ⊢φ→∀x∈AB∈ℝ
6 nfra1 ⊢Ⅎx∀x∈AB∈ℝ
7 nfv ⊢Ⅎxz∈ℝ
8 simp3 ⊢∀x∈AB∈ℝ∧x∈A∧z=B→z=B
9 rspa ⊢∀x∈AB∈ℝ∧x∈A→B∈ℝ
10 9 3adant3 ⊢∀x∈AB∈ℝ∧x∈A∧z=B→B∈ℝ
11 8 10 eqeltrd ⊢∀x∈AB∈ℝ∧x∈A∧z=B→z∈ℝ
12 11 3exp ⊢∀x∈AB∈ℝ→x∈A→z=B→z∈ℝ
13 6 7 12 rexlimd ⊢∀x∈AB∈ℝ→∃x∈Az=B→z∈ℝ
14 13 abssdv ⊢∀x∈AB∈ℝ→z|∃x∈Az=B⊆ℝ
15 5 14 syl ⊢φ→z|∃x∈Az=B⊆ℝ
16 eqidd ⊢x∈A→B=B
17 16 rgen ⊢∀x∈AB=B
18 r19.2z ⊢A≠∅∧∀x∈AB=B→∃x∈AB=B
19 1 17 18 sylancl ⊢φ→∃x∈AB=B
20 nfv ⊢Ⅎxφ
21 nfre1 ⊢Ⅎx∃x∈Az=B
22 21 nfex ⊢Ⅎx∃z∃x∈Az=B
23 simpr ⊢φ∧x∈A→x∈A
24 elex ⊢B∈ℝ→B∈V
25 2 24 syl ⊢φ∧x∈A→B∈V
26 isset ⊢B∈V↔∃zz=B
27 25 26 sylib ⊢φ∧x∈A→∃zz=B
28 rspe ⊢x∈A∧∃zz=B→∃x∈A∃zz=B
29 23 27 28 syl2anc ⊢φ∧x∈A→∃x∈A∃zz=B
30 rexcom4 ⊢∃x∈A∃zz=B↔∃z∃x∈Az=B
31 29 30 sylib ⊢φ∧x∈A→∃z∃x∈Az=B
32 31 3adant3 ⊢φ∧x∈A∧B=B→∃z∃x∈Az=B
33 32 3exp ⊢φ→x∈A→B=B→∃z∃x∈Az=B
34 20 22 33 rexlimd ⊢φ→∃x∈AB=B→∃z∃x∈Az=B
35 19 34 mpd ⊢φ→∃z∃x∈Az=B
36 abn0 ⊢z|∃x∈Az=B≠∅↔∃z∃x∈Az=B
37 35 36 sylibr ⊢φ→z|∃x∈Az=B≠∅
38 vex ⊢w∈V
39 eqeq1 ⊢z=w→z=B↔w=B
40 39 rexbidv ⊢z=w→∃x∈Az=B↔∃x∈Aw=B
41 38 40 elab ⊢w∈z|∃x∈Az=B↔∃x∈Aw=B
42 41 biimpi ⊢w∈z|∃x∈Az=B→∃x∈Aw=B
43 42 adantl ⊢φ∧∀x∈AB≤y∧w∈z|∃x∈Az=B→∃x∈Aw=B
44 nfra1 ⊢Ⅎx∀x∈AB≤y
45 20 44 nfan ⊢Ⅎxφ∧∀x∈AB≤y
46 21 nfsab ⊢Ⅎxw∈z|∃x∈Az=B
47 45 46 nfan ⊢Ⅎxφ∧∀x∈AB≤y∧w∈z|∃x∈Az=B
48 nfv ⊢Ⅎxw≤y
49 simp3 ⊢φ∧∀x∈AB≤y∧x∈A∧w=B→w=B
50 simp1r ⊢φ∧∀x∈AB≤y∧x∈A∧w=B→∀x∈AB≤y
51 simp2 ⊢φ∧∀x∈AB≤y∧x∈A∧w=B→x∈A
52 rspa ⊢∀x∈AB≤y∧x∈A→B≤y
53 50 51 52 syl2anc ⊢φ∧∀x∈AB≤y∧x∈A∧w=B→B≤y
54 49 53 eqbrtrd ⊢φ∧∀x∈AB≤y∧x∈A∧w=B→w≤y
55 54 3exp ⊢φ∧∀x∈AB≤y→x∈A→w=B→w≤y
56 55 adantr ⊢φ∧∀x∈AB≤y∧w∈z|∃x∈Az=B→x∈A→w=B→w≤y
57 47 48 56 rexlimd ⊢φ∧∀x∈AB≤y∧w∈z|∃x∈Az=B→∃x∈Aw=B→w≤y
58 43 57 mpd ⊢φ∧∀x∈AB≤y∧w∈z|∃x∈Az=B→w≤y
59 58 ralrimiva ⊢φ∧∀x∈AB≤y→∀w∈z|∃x∈Az=Bw≤y
60 59 3adant2 ⊢φ∧y∈ℝ∧∀x∈AB≤y→∀w∈z|∃x∈Az=Bw≤y
61 60 3exp ⊢φ→y∈ℝ→∀x∈AB≤y→∀w∈z|∃x∈Az=Bw≤y
62 61 reximdvai ⊢φ→∃y∈ℝ∀x∈AB≤y→∃y∈ℝ∀w∈z|∃x∈Az=Bw≤y
63 3 62 mpd ⊢φ→∃y∈ℝ∀w∈z|∃x∈Az=Bw≤y
64 suprcl ⊢z|∃x∈Az=B⊆ℝ∧z|∃x∈Az=B≠∅∧∃y∈ℝ∀w∈z|∃x∈Az=Bw≤y→supz|∃x∈Az=Bℝ<∈ℝ
65 15 37 63 64 syl3anc ⊢φ→supz|∃x∈Az=Bℝ<∈ℝ
66 4 65 eqeltrid ⊢φ→C∈ℝ
67 15 adantr ⊢φ∧x∈A→z|∃x∈Az=B⊆ℝ
68 31 36 sylibr ⊢φ∧x∈A→z|∃x∈Az=B≠∅
69 63 adantr ⊢φ∧x∈A→∃y∈ℝ∀w∈z|∃x∈Az=Bw≤y
70 elabrexg ⊢x∈A∧B∈ℝ→B∈z|∃x∈Az=B
71 23 2 70 syl2anc ⊢φ∧x∈A→B∈z|∃x∈Az=B
72 suprub ⊢z|∃x∈Az=B⊆ℝ∧z|∃x∈Az=B≠∅∧∃y∈ℝ∀w∈z|∃x∈Az=Bw≤y∧B∈z|∃x∈Az=B→B≤supz|∃x∈Az=Bℝ<
73 67 68 69 71 72 syl31anc ⊢φ∧x∈A→B≤supz|∃x∈Az=Bℝ<
74 73 4 breqtrrdi ⊢φ∧x∈A→B≤C
75 74 ralrimiva ⊢φ→∀x∈AB≤C
76 66 75 jca ⊢φ→C∈ℝ∧∀x∈AB≤C