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 biimpi ⊢ w ∈ z | ∃ x ∈ A z = B → ∃ x ∈ A w = B
43 42 adantl ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ w ∈ z | ∃ x ∈ A z = B → ∃ x ∈ A w = B
44 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ≤ y
45 20 44 nfan ⊢ Ⅎ x φ ∧ ∀ x ∈ A B ≤ y
46 21 nfsab ⊢ Ⅎ x w ∈ z | ∃ x ∈ A z = B
47 45 46 nfan ⊢ Ⅎ x φ ∧ ∀ x ∈ A B ≤ y ∧ w ∈ z | ∃ x ∈ A z = B
48 nfv ⊢ Ⅎ x w ≤ y
49 simp3 ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ w = B → w = B
50 simp1r ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ w = B → ∀ x ∈ A B ≤ y
51 simp2 ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ w = B → x ∈ A
52 rspa ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A → B ≤ y
53 50 51 52 syl2anc ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ w = B → B ≤ y
54 49 53 eqbrtrd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ w = B → w ≤ y
55 54 3exp ⊢ φ ∧ ∀ x ∈ A B ≤ y → x ∈ A → w = B → w ≤ y
56 55 adantr ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ w ∈ z | ∃ x ∈ A z = B → x ∈ A → w = B → w ≤ y
57 47 48 56 rexlimd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ w ∈ z | ∃ x ∈ A z = B → ∃ x ∈ A w = B → w ≤ y
58 43 57 mpd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ w ∈ z | ∃ x ∈ A z = B → w ≤ y
59 58 ralrimiva ⊢ φ ∧ ∀ x ∈ A B ≤ y → ∀ w ∈ z | ∃ x ∈ A z = B w ≤ y
60 59 3adant2 ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∀ w ∈ z | ∃ x ∈ A z = B w ≤ y
61 60 3exp ⊢ φ → y ∈ ℝ → ∀ x ∈ A B ≤ y → ∀ w ∈ z | ∃ x ∈ A z = B w ≤ y
62 61 reximdvai ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ w ∈ z | ∃ x ∈ A z = B w ≤ y
63 3 62 mpd ⊢ φ → ∃ y ∈ ℝ ∀ w ∈ z | ∃ x ∈ A z = B w ≤ y
64 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 ℝ < ∈ ℝ
65 15 37 63 64 syl3anc ⊢ φ → sup z | ∃ x ∈ A z = B ℝ < ∈ ℝ
66 4 65 eqeltrid ⊢ φ → C ∈ ℝ
67 15 adantr ⊢ φ ∧ x ∈ A → z | ∃ x ∈ A z = B ⊆ ℝ
68 31 36 sylibr ⊢ φ ∧ x ∈ A → z | ∃ x ∈ A z = B ≠ ∅
69 63 adantr ⊢ φ ∧ x ∈ A → ∃ y ∈ ℝ ∀ w ∈ z | ∃ x ∈ A z = B w ≤ y
70 elabrexg ⊢ x ∈ A ∧ B ∈ ℝ → B ∈ z | ∃ x ∈ A z = B
71 23 2 70 syl2anc ⊢ φ ∧ x ∈ A → B ∈ z | ∃ x ∈ A z = B
72 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 ℝ <
73 67 68 69 71 72 syl31anc ⊢ φ ∧ x ∈ A → B ≤ sup z | ∃ x ∈ A z = B ℝ <
74 73 4 breqtrrdi ⊢ φ ∧ x ∈ A → B ≤ C
75 74 ralrimiva ⊢ φ → ∀ x ∈ A B ≤ C
76 66 75 jca ⊢ φ → C ∈ ℝ ∧ ∀ x ∈ A B ≤ C