Metamath Proof Explorer


Theorem hoidmv1lelem1

Description: The supremum of U belongs to U . This is the last part of step (a) and the whole step (b) in the proof of Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1lelem1.a φ A
hoidmv1lelem1.b φ B
hoidmv1lelem1.l φ A < B
hoidmv1lelem1.c φ C :
hoidmv1lelem1.d φ D :
hoidmv1lelem1.r φ sum^ j vol C j D j
hoidmv1lelem1.u U = z A B | z A sum^ j vol C j if D j z D j z
hoidmv1lelem1.s S = sup U <
Assertion hoidmv1lelem1 φ S U A U x y U y x

Proof

Step Hyp Ref Expression
1 hoidmv1lelem1.a φ A
2 hoidmv1lelem1.b φ B
3 hoidmv1lelem1.l φ A < B
4 hoidmv1lelem1.c φ C :
5 hoidmv1lelem1.d φ D :
6 hoidmv1lelem1.r φ sum^ j vol C j D j
7 hoidmv1lelem1.u U = z A B | z A sum^ j vol C j if D j z D j z
8 hoidmv1lelem1.s S = sup U <
9 ssrab2 z A B | z A sum^ j vol C j if D j z D j z A B
10 7 9 eqsstri U A B
11 10 a1i φ U A B
12 1 rexrd φ A *
13 2 rexrd φ B *
14 1 2 3 ltled φ A B
15 lbicc2 A * B * A B A A B
16 12 13 14 15 syl3anc φ A A B
17 1 recnd φ A
18 17 subidd φ A A = 0
19 nfv j φ
20 nnex V
21 20 a1i φ V
22 volf vol : dom vol 0 +∞
23 22 a1i φ j vol : dom vol 0 +∞
24 4 ffvelrnda φ j C j
25 5 ffvelrnda φ j D j
26 1 adantr φ j A
27 25 26 ifcld φ j if D j A D j A
28 27 rexrd φ j if D j A D j A *
29 icombl C j if D j A D j A * C j if D j A D j A dom vol
30 24 28 29 syl2anc φ j C j if D j A D j A dom vol
31 23 30 ffvelrnd φ j vol C j if D j A D j A 0 +∞
32 19 21 31 sge0ge0mpt φ 0 sum^ j vol C j if D j A D j A
33 18 32 eqbrtrd φ A A sum^ j vol C j if D j A D j A
34 16 33 jca φ A A B A A sum^ j vol C j if D j A D j A
35 oveq1 z = A z A = A A
36 breq2 z = A D j z D j A
37 id z = A z = A
38 36 37 ifbieq2d z = A if D j z D j z = if D j A D j A
39 38 oveq2d z = A C j if D j z D j z = C j if D j A D j A
40 39 fveq2d z = A vol C j if D j z D j z = vol C j if D j A D j A
41 40 mpteq2dv z = A j vol C j if D j z D j z = j vol C j if D j A D j A
42 41 fveq2d z = A sum^ j vol C j if D j z D j z = sum^ j vol C j if D j A D j A
43 35 42 breq12d z = A z A sum^ j vol C j if D j z D j z A A sum^ j vol C j if D j A D j A
44 43 elrab A z A B | z A sum^ j vol C j if D j z D j z A A B A A sum^ j vol C j if D j A D j A
45 34 44 sylibr φ A z A B | z A sum^ j vol C j if D j z D j z
46 45 7 eleqtrrdi φ A U
47 46 ne0d φ U
48 1 2 11 47 supicc φ sup U < A B
49 8 48 eqeltrid φ S A B
50 8 a1i φ S = sup U <
51 nfv z φ
52 1 2 iccssred φ A B
53 11 52 sstrd φ U
54 53 sselda φ z U z
55 nfv j φ z U
56 20 a1i φ z U V
57 22 a1i φ z U j vol : dom vol 0 +∞
58 24 adantlr φ z U j C j
59 25 adantlr φ z U j D j
60 54 adantr φ z U j z
61 59 60 ifcld φ z U j if D j z D j z
62 61 rexrd φ z U j if D j z D j z *
63 icombl C j if D j z D j z * C j if D j z D j z dom vol
64 58 62 63 syl2anc φ z U j C j if D j z D j z dom vol
65 57 64 ffvelrnd φ z U j vol C j if D j z D j z 0 +∞
66 55 56 65 sge0xrclmpt φ z U sum^ j vol C j if D j z D j z *
67 pnfxr +∞ *
68 67 a1i φ z U +∞ *
69 6 rexrd φ sum^ j vol C j D j *
70 69 adantr φ z U sum^ j vol C j D j *
71 25 rexrd φ j D j *
72 icombl C j D j * C j D j dom vol
73 24 71 72 syl2anc φ j C j D j dom vol
74 23 73 ffvelrnd φ j vol C j D j 0 +∞
75 74 adantlr φ z U j vol C j D j 0 +∞
76 73 adantlr φ z U j C j D j dom vol
77 24 rexrd φ j C j *
78 77 adantlr φ z U j C j *
79 71 adantlr φ z U j D j *
80 24 leidd φ j C j C j
81 80 adantlr φ z U j C j C j
82 min1 D j z if D j z D j z D j
83 59 60 82 syl2anc φ z U j if D j z D j z D j
84 icossico C j * D j * C j C j if D j z D j z D j C j if D j z D j z C j D j
85 78 79 81 83 84 syl22anc φ z U j C j if D j z D j z C j D j
86 volss C j if D j z D j z dom vol C j D j dom vol C j if D j z D j z C j D j vol C j if D j z D j z vol C j D j
87 64 76 85 86 syl3anc φ z U j vol C j if D j z D j z vol C j D j
88 55 56 65 75 87 sge0lempt φ z U sum^ j vol C j if D j z D j z sum^ j vol C j D j
89 6 ltpnfd φ sum^ j vol C j D j < +∞
90 89 adantr φ z U sum^ j vol C j D j < +∞
91 66 70 68 88 90 xrlelttrd φ z U sum^ j vol C j if D j z D j z < +∞
92 66 68 91 xrltned φ z U sum^ j vol C j if D j z D j z +∞
93 92 neneqd φ z U ¬ sum^ j vol C j if D j z D j z = +∞
94 eqid j vol C j if D j z D j z = j vol C j if D j z D j z
95 65 94 fmptd φ z U j vol C j if D j z D j z : 0 +∞
96 56 95 sge0repnf φ z U sum^ j vol C j if D j z D j z ¬ sum^ j vol C j if D j z D j z = +∞
97 93 96 mpbird φ z U sum^ j vol C j if D j z D j z
98 1 adantr φ z U A
99 97 98 readdcld φ z U sum^ j vol C j if D j z D j z + A
100 52 49 sseldd φ S
101 100 adantr φ j S
102 25 101 ifcld φ j if D j S D j S
103 102 rexrd φ j if D j S D j S *
104 icombl C j if D j S D j S * C j if D j S D j S dom vol
105 24 103 104 syl2anc φ j C j if D j S D j S dom vol
106 23 105 ffvelrnd φ j vol C j if D j S D j S 0 +∞
107 19 21 106 sge0xrclmpt φ sum^ j vol C j if D j S D j S *
108 67 a1i φ +∞ *
109 min1 D j S if D j S D j S D j
110 25 101 109 syl2anc φ j if D j S D j S D j
111 icossico C j * D j * C j C j if D j S D j S D j C j if D j S D j S C j D j
112 77 71 80 110 111 syl22anc φ j C j if D j S D j S C j D j
113 volss C j if D j S D j S dom vol C j D j dom vol C j if D j S D j S C j D j vol C j if D j S D j S vol C j D j
114 105 73 112 113 syl3anc φ j vol C j if D j S D j S vol C j D j
115 19 21 106 74 114 sge0lempt φ sum^ j vol C j if D j S D j S sum^ j vol C j D j
116 107 69 108 115 89 xrlelttrd φ sum^ j vol C j if D j S D j S < +∞
117 107 108 116 xrltned φ sum^ j vol C j if D j S D j S +∞
118 117 neneqd φ ¬ sum^ j vol C j if D j S D j S = +∞
119 eqid j vol C j if D j S D j S = j vol C j if D j S D j S
120 106 119 fmptd φ j vol C j if D j S D j S : 0 +∞
121 21 120 sge0repnf φ sum^ j vol C j if D j S D j S ¬ sum^ j vol C j if D j S D j S = +∞
122 118 121 mpbird φ sum^ j vol C j if D j S D j S
123 122 1 readdcld φ sum^ j vol C j if D j S D j S + A
124 123 adantr φ z U sum^ j vol C j if D j S D j S + A
125 7 eleq2i z U z z A B | z A sum^ j vol C j if D j z D j z
126 125 biimpi z U z z A B | z A sum^ j vol C j if D j z D j z
127 126 adantl φ z U z z A B | z A sum^ j vol C j if D j z D j z
128 rabid z z A B | z A sum^ j vol C j if D j z D j z z A B z A sum^ j vol C j if D j z D j z
129 127 128 sylib φ z U z A B z A sum^ j vol C j if D j z D j z
130 129 simprd φ z U z A sum^ j vol C j if D j z D j z
131 54 98 97 lesubaddd φ z U z A sum^ j vol C j if D j z D j z z sum^ j vol C j if D j z D j z + A
132 130 131 mpbid φ z U z sum^ j vol C j if D j z D j z + A
133 122 adantr φ z U sum^ j vol C j if D j S D j S
134 106 adantlr φ z U j vol C j if D j S D j S 0 +∞
135 105 adantlr φ z U j C j if D j S D j S dom vol
136 103 adantlr φ z U j if D j S D j S *
137 61 adantr φ z U j D j z if D j z D j z
138 eqidd φ z U j D j z D j = D j
139 iftrue D j z if D j z D j z = D j
140 139 adantl φ z U j D j z if D j z D j z = D j
141 59 adantr φ z U j D j z D j
142 60 adantr φ z U j D j z z
143 100 ad3antrrr φ z U j D j z S
144 simpr φ z U j D j z D j z
145 53 adantr φ z U U
146 47 adantr φ z U U
147 1 2 jca φ A B
148 iccsupr A B U A B A U U U x y U y x
149 147 11 46 148 syl3anc φ U U x y U y x
150 149 simp3d φ x y U y x
151 150 adantr φ z U x y U y x
152 127 125 sylibr φ z U z U
153 suprub U U x y U y x z U z sup U <
154 145 146 151 152 153 syl31anc φ z U z sup U <
155 154 8 breqtrrdi φ z U z S
156 155 ad2antrr φ z U j D j z z S
157 141 142 143 144 156 letrd φ z U j D j z D j S
158 157 iftrued φ z U j D j z if D j S D j S = D j
159 138 140 158 3eqtr4d φ z U j D j z if D j z D j z = if D j S D j S
160 137 159 eqled φ z U j D j z if D j z D j z if D j S D j S
161 60 adantr φ z U j ¬ D j z z
162 59 adantr φ z U j ¬ D j z D j
163 simpr φ z U j ¬ D j z ¬ D j z
164 161 162 ltnled φ z U j ¬ D j z z < D j ¬ D j z
165 163 164 mpbird φ z U j ¬ D j z z < D j
166 161 162 165 ltled φ z U j ¬ D j z z D j
167 166 adantr φ z U j ¬ D j z D j S z D j
168 iffalse ¬ D j z if D j z D j z = z
169 168 ad2antlr φ z U j ¬ D j z D j S if D j z D j z = z
170 iftrue D j S if D j S D j S = D j
171 170 adantl φ z U j ¬ D j z D j S if D j S D j S = D j
172 169 171 breq12d φ z U j ¬ D j z D j S if D j z D j z if D j S D j S z D j
173 167 172 mpbird φ z U j ¬ D j z D j S if D j z D j z if D j S D j S
174 155 ad3antrrr φ z U j ¬ D j z ¬ D j S z S
175 168 ad2antlr φ z U j ¬ D j z ¬ D j S if D j z D j z = z
176 iffalse ¬ D j S if D j S D j S = S
177 176 adantl φ z U j ¬ D j z ¬ D j S if D j S D j S = S
178 175 177 breq12d φ z U j ¬ D j z ¬ D j S if D j z D j z if D j S D j S z S
179 174 178 mpbird φ z U j ¬ D j z ¬ D j S if D j z D j z if D j S D j S
180 173 179 pm2.61dan φ z U j ¬ D j z if D j z D j z if D j S D j S
181 160 180 pm2.61dan φ z U j if D j z D j z if D j S D j S
182 icossico C j * if D j S D j S * C j C j if D j z D j z if D j S D j S C j if D j z D j z C j if D j S D j S
183 78 136 81 181 182 syl22anc φ z U j C j if D j z D j z C j if D j S D j S
184 volss C j if D j z D j z dom vol C j if D j S D j S dom vol C j if D j z D j z C j if D j S D j S vol C j if D j z D j z vol C j if D j S D j S
185 64 135 183 184 syl3anc φ z U j vol C j if D j z D j z vol C j if D j S D j S
186 55 56 65 134 185 sge0lempt φ z U sum^ j vol C j if D j z D j z sum^ j vol C j if D j S D j S
187 97 133 98 186 leadd1dd φ z U sum^ j vol C j if D j z D j z + A sum^ j vol C j if D j S D j S + A
188 54 99 124 132 187 letrd φ z U z sum^ j vol C j if D j S D j S + A
189 188 ex φ z U z sum^ j vol C j if D j S D j S + A
190 51 189 ralrimi φ z U z sum^ j vol C j if D j S D j S + A
191 suprleub U U x y U y x sum^ j vol C j if D j S D j S + A sup U < sum^ j vol C j if D j S D j S + A z U z sum^ j vol C j if D j S D j S + A
192 53 47 150 123 191 syl31anc φ sup U < sum^ j vol C j if D j S D j S + A z U z sum^ j vol C j if D j S D j S + A
193 190 192 mpbird φ sup U < sum^ j vol C j if D j S D j S + A
194 50 193 eqbrtrd φ S sum^ j vol C j if D j S D j S + A
195 100 1 122 lesubaddd φ S A sum^ j vol C j if D j S D j S S sum^ j vol C j if D j S D j S + A
196 194 195 mpbird φ S A sum^ j vol C j if D j S D j S
197 49 196 jca φ S A B S A sum^ j vol C j if D j S D j S
198 oveq1 z = S z A = S A
199 breq2 z = S D j z D j S
200 id z = S z = S
201 199 200 ifbieq2d z = S if D j z D j z = if D j S D j S
202 201 oveq2d z = S C j if D j z D j z = C j if D j S D j S
203 202 fveq2d z = S vol C j if D j z D j z = vol C j if D j S D j S
204 203 mpteq2dv z = S j vol C j if D j z D j z = j vol C j if D j S D j S
205 204 fveq2d z = S sum^ j vol C j if D j z D j z = sum^ j vol C j if D j S D j S
206 198 205 breq12d z = S z A sum^ j vol C j if D j z D j z S A sum^ j vol C j if D j S D j S
207 206 elrab S z A B | z A sum^ j vol C j if D j z D j z S A B S A sum^ j vol C j if D j S D j S
208 197 207 sylibr φ S z A B | z A sum^ j vol C j if D j z D j z
209 208 7 eleqtrrdi φ S U
210 209 46 150 3jca φ S U A U x y U y x