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 ∈ A B ≤ y
upbdrech.c ⊢ C = sup z | ∃ x ∈ A z = B ℝ <
Assertion upbdrech ⊢ φ → C ∈ ℝ ∧ ∀ x ∈ A B ≤ C

Proof

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