Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem31 Structured version   Unicode version

Theorem stoweidlem31 27756
 Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that is a finite subset of , indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on . Here M is used to represent m in the paper, is used to represent ε in the paper, vi is used to represent V(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem31.1
stoweidlem31.2
stoweidlem31.3
stoweidlem31.4
stoweidlem31.5
stoweidlem31.6
stoweidlem31.7
stoweidlem31.8
stoweidlem31.9
stoweidlem31.10
stoweidlem31.11
stoweidlem31.12
stoweidlem31.13
stoweidlem31.14
Assertion
Ref Expression
stoweidlem31
Distinct variable groups:   ,,,,   ,   ,   ,   ,,,,   ,,,,   ,,,,   ,,,   ,,,   ,,,   ,,,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,,,)   (,,)   (,,,,,)   (,,,)   (,,,)   (,,,)   (,)   (,,,,)   (,,,,,,)   ()   (,,,,,,)   (,,,,)

Proof of Theorem stoweidlem31
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem31.14 . . 3
2 fnchoice 27676 . . 3
31, 2syl 16 . 2
4 vex 2959 . . . . 5
5 stoweidlem31.6 . . . . . . 7
6 stoweidlem31.12 . . . . . . . . 9
7 stoweidlem31.7 . . . . . . . . 9
86, 7ssexd 4350 . . . . . . . 8
9 mptexg 5965 . . . . . . . 8
108, 9syl 16 . . . . . . 7
115, 10syl5eqel 2520 . . . . . 6
12 vex 2959 . . . . . 6
13 coexg 5412 . . . . . 6
1411, 12, 13sylancl 644 . . . . 5
15 coexg 5412 . . . . 5
164, 14, 15sylancr 645 . . . 4
18 simprl 733 . . . . . 6
19 stoweidlem31.1 . . . . . . . . 9
20 nfcv 2572 . . . . . . . . . . 11
21 nfcv 2572 . . . . . . . . . . . . . 14
22 nfrab1 2888 . . . . . . . . . . . . . 14
2321, 22nfmpt 4297 . . . . . . . . . . . . 13
245, 23nfcxfr 2569 . . . . . . . . . . . 12
2524nfrn 5112 . . . . . . . . . . 11
2620, 25nffn 5541 . . . . . . . . . 10
27 nfv 1629 . . . . . . . . . . 11
2825, 27nfral 2759 . . . . . . . . . 10
2926, 28nfan 1846 . . . . . . . . 9
3019, 29nfan 1846 . . . . . . . 8
31 fvelrnb 5774 . . . . . . . . . . . . 13
3218, 31syl 16 . . . . . . . . . . . 12
3332biimpa 471 . . . . . . . . . . 11
34 nfv 1629 . . . . . . . . . . . . . 14
35 nfv 1629 . . . . . . . . . . . . . . 15
36 nfra1 2756 . . . . . . . . . . . . . . 15
3735, 36nfan 1846 . . . . . . . . . . . . . 14
3834, 37nfan 1846 . . . . . . . . . . . . 13
39 nfv 1629 . . . . . . . . . . . . 13
4038, 39nfan 1846 . . . . . . . . . . . 12
41 simp3 959 . . . . . . . . . . . . . 14
42 simp1ll 1020 . . . . . . . . . . . . . . 15
43 simplrr 738 . . . . . . . . . . . . . . . 16
44433ad2ant1 978 . . . . . . . . . . . . . . 15
45 simp2 958 . . . . . . . . . . . . . . 15
46 simp3 959 . . . . . . . . . . . . . . . . 17
47 3simpc 956 . . . . . . . . . . . . . . . . . 18
48 simpr 448 . . . . . . . . . . . . . . . . . . . . 21
49 stoweidlem31.3 . . . . . . . . . . . . . . . . . . . . . . . . 25
50 stoweidlem31.13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
51 rabexg 4353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5250, 51syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5352a1d 23 . . . . . . . . . . . . . . . . . . . . . . . . 25
5449, 53ralrimi 2787 . . . . . . . . . . . . . . . . . . . . . . . 24
555fnmpt 5571 . . . . . . . . . . . . . . . . . . . . . . . 24
5654, 55syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
5756adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
58 fvelrnb 5774 . . . . . . . . . . . . . . . . . . . . . . 23
59 nfmpt1 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
605, 59nfcxfr 2569 . . . . . . . . . . . . . . . . . . . . . . . . . 26
61 nfcv 2572 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6260, 61nffv 5735 . . . . . . . . . . . . . . . . . . . . . . . . 25
63 nfcv 2572 . . . . . . . . . . . . . . . . . . . . . . . . 25
6462, 63nfeq 2579 . . . . . . . . . . . . . . . . . . . . . . . 24
65 nfv 1629 . . . . . . . . . . . . . . . . . . . . . . . 24
66 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . 25
6766eqeq1d 2444 . . . . . . . . . . . . . . . . . . . . . . . 24
6864, 65, 67cbvrex 2929 . . . . . . . . . . . . . . . . . . . . . . 23
6958, 68syl6bb 253 . . . . . . . . . . . . . . . . . . . . . 22
7057, 69syl 16 . . . . . . . . . . . . . . . . . . . . 21
7148, 70mpbid 202 . . . . . . . . . . . . . . . . . . . 20
7260nfrn 5112 . . . . . . . . . . . . . . . . . . . . . . 23
7372nfcri 2566 . . . . . . . . . . . . . . . . . . . . . 22
7449, 73nfan 1846 . . . . . . . . . . . . . . . . . . . . 21
75 nfv 1629 . . . . . . . . . . . . . . . . . . . . 21
76 simp3 959 . . . . . . . . . . . . . . . . . . . . . . . 24
77 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7850adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7978, 51syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
805fvmpt2 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8177, 79, 80syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
827sselda 3348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
83 stoweidlem31.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8483rabeq2i 2953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8582, 84sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8685simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87 stoweidlem31.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
88 stoweidlem31.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8988nnrpd 10647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9087, 89rpdivcld 10665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9190adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92 breq2 4216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9392ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94 oveq2 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9594breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9695ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9793, 963anbi23d 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9897rexbidv 2726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9998rspccva 3051 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10086, 91, 99syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
101 nfv 1629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10219, 101nfan 1846 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103 nfcv 2572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10422, 103nfne 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105 3simpc 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106 rabid 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
107105, 106sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
108 ne0i 3634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109107, 108syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1101093exp 1152 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111102, 104, 110rexlimd 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
112100, 111mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11381, 112eqnetrd 2619 . . . . . . . . . . . . . . . . . . . . . . . . 25
1141133adant3 977 . . . . . . . . . . . . . . . . . . . . . . . 24
11576, 114eqnetrrd 2621 . . . . . . . . . . . . . . . . . . . . . . 23
1161153adant1r 1177 . . . . . . . . . . . . . . . . . . . . . 22
1171163exp 1152 . . . . . . . . . . . . . . . . . . . . 21
11874, 75, 117rexlimd 2827 . . . . . . . . . . . . . . . . . . . 20
11971, 118mpd 15 . . . . . . . . . . . . . . . . . . 19
1201193adant2 976 . . . . . . . . . . . . . . . . . 18
121 rsp 2766 . . . . . . . . . . . . . . . . . . 19
122121imp 419 . . . . . . . . . . . . . . . . . 18
12347, 120, 122sylc 58 . . . . . . . . . . . . . . . . 17
12446, 123jca 519 . . . . . . . . . . . . . . . 16
125 vex 2959 . . . . . . . . . . . . . . . . . 18
1265elrnmpt 5117 . . . . . . . . . . . . . . . . . 18
127125, 126ax-mp 8 . . . . . . . . . . . . . . . . 17
12846, 127sylib 189 . . . . . . . . . . . . . . . 16
129 nfv 1629 . . . . . . . . . . . . . . . . . 18
13073, 129nfan 1846 . . . . . . . . . . . . . . . . 17
131 nfv 1629 . . . . . . . . . . . . . . . . 17
132 simp1r 982 . . . . . . . . . . . . . . . . . . 19
133 simp3 959 . . . . . . . . . . . . . . . . . . 19
134 simpl 444 . . . . . . . . . . . . . . . . . . . . . 22
135 simpr 448 . . . . . . . . . . . . . . . . . . . . . 22
136134, 135eleqtrd 2512 . . . . . . . . . . . . . . . . . . . . 21
137 elrabi 3090 . . . . . . . . . . . . . . . . . . . . . 22
138 fveq1 5727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
139138breq2d 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140138breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
141139, 140anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
142141ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
143138breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
144143ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
145138breq2d 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
146145ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
147142, 144, 1463anbi123d 1254 . . . . . . . . . . . . . . . . . . . . . . . . 25
148147elrab 3092 . . . . . . . . . . . . . . . . . . . . . . . 24
149148simprbi 451 . . . . . . . . . . . . . . . . . . . . . . 23
150149simp1d 969 . . . . . . . . . . . . . . . . . . . . . 22
151142elrab 3092 . . . . . . . . . . . . . . . . . . . . . 22
152137, 150, 151sylanbrc 646 . . . . . . . . . . . . . . . . . . . . 21
153136, 152syl 16 . . . . . . . . . . . . . . . . . . . 20
154 stoweidlem31.4 . . . . . . . . . . . . . . . . . . . 20
155153, 154syl6eleqr 2527 . . . . . . . . . . . . . . . . . . 19
156132, 133, 155syl2anc 643 . . . . . . . . . . . . . . . . . 18
1571563exp 1152 . . . . . . . . . . . . . . . . 17
158130, 131, 157rexlimd 2827 . . . . . . . . . . . . . . . 16
159124, 128, 158sylc 58 . . . . . . . . . . . . . . 15
16042, 44, 45, 159syl3anc 1184 . . . . . . . . . . . . . 14
16141, 160eqeltrrd 2511 . . . . . . . . . . . . 13
1621613exp 1152 . . . . . . . . . . . 12
16340, 162reximdai 2814 . . . . . . . . . . 11
16433, 163mpd 15 . . . . . . . . . 10
165 nfv 1629 . . . . . . . . . . 11
166 idd 22 . . . . . . . . . . . 12
167166a1i 11 . . . . . . . . . . 11
16840, 165, 167rexlimd 2827 . . . . . . . . . 10
169164, 168mpd 15 . . . . . . . . 9
170169ex 424 . . . . . . . 8
17130, 170ralrimi 2787 . . . . . . 7
172 dfss3 3338 . . . . . . . 8
173 nfrab1 2888 . . . . . . . . . . 11
174154, 173nfcxfr 2569 . . . . . . . . . 10
175174nfcri 2566 . . . . . . . . 9
176 nfv 1629 . . . . . . . . 9
177 eleq1 2496 . . . . . . . . 9
178175, 176, 177cbvral 2928 . . . . . . . 8
179172, 178bitri 241 . . . . . . 7
180171, 179sylibr 204 . . . . . 6
181 df-f 5458 . . . . . 6
18218, 180, 181sylanbrc 646 . . . . 5
183 dffn3 5598 . . . . . . . 8
18456, 183sylib 189 . . . . . . 7
185184adantr 452 . . . . . 6
186 stoweidlem31.9 . . . . . . . 8
187 f1of 5674 . . . . . . . 8
188186, 187syl 16 . . . . . . 7
189188adantr 452 . . . . . 6
190 fco 5600 . . . . . 6
191185, 189, 190syl2anc 643 . . . . 5
192 fco 5600 . . . . 5
193182, 191, 192syl2anc 643 . . . 4
194 fvco3 5800 . . . . . . . . 9
195191, 194sylan 458 . . . . . . . 8
196 simpll 731 . . . . . . . . 9
197 simplrr 738 . . . . . . . . 9
198191fnvinran 27661 . . . . . . . . 9
199 simp3 959 . . . . . . . . . 10
200 nfcv 2572 . . . . . . . . . . 11
201 nfv 1629 . . . . . . . . . . . . 13
20234, 36, 201nf3an 1849 . . . . . . . . . . . 12
203 nfv 1629 . . . . . . . . . . . 12
204202, 203nfim 1832 . . . . . . . . . . 11
205 eleq1 2496 . . . . . . . . . . . . 13
2062053anbi3d 1260 . . . . . . . . . . . 12
207 fveq2 5728 . . . . . . . . . . . . 13
208 id 20 . . . . . . . . . . . . 13
209207, 208eleq12d 2504 . . . . . . . . . . . 12
210206, 209imbi12d 312 . . . . . . . . . . 11
211200, 204, 210, 123vtoclgf 3010 . . . . . . . . . 10
212199, 211mpcom 34 . . . . . . . . 9
213196, 197, 198, 212syl3anc 1184 . . . . . . . 8
214195, 213eqeltrd 2510 . . . . . . 7
215 fvco3 5800 . . . . . . . . . . . 12
216188, 215sylan 458 . . . . . . . . . . 11
217188fnvinran 27661 . . . . . . . . . . . 12
21850adantr 452 . . . . . . . . . . . . 13
219 rabexg 4353 . . . . . . . . . . . . 13
220218, 219syl 16 . . . . . . . . . . . 12
221 raleq 2904 . . . . . . . . . . . . . . 15
2222213anbi2d 1259 . . . . . . . . . . . . . 14
223222rabbidv 2948 . . . . . . . . . . . . 13
224223, 5fvmptg 5804 . . . . . . . . . . . 12
225217, 220, 224syl2anc 643 . . . . . . . . . . 11
226216, 225eqtrd 2468 . . . . . . . . . 10
227226adantlr 696 . . . . . . . . 9
228227eleq2d 2503 . . . . . . . 8
229 nfcv 2572 . . . . . . . . . . . . . 14
23024, 229nfco 5038 . . . . . . . . . . . . 13
23120, 230nfco 5038 . . . . . . . . . . . 12
232 nfcv 2572 . . . . . . . . . . . 12
233231, 232nffv 5735 . . . . . . . . . . 11
234 nfcv 2572 . . . . . . . . . . 11
235 nfcv 2572 . . . . . . . . . . . . 13
236 nfcv 2572 . . . . . . . . . . . . . . 15
237 nfcv 2572 . . . . . . . . . . . . . . 15
238 nfcv 2572 . . . . . . . . . . . . . . . 16
239233, 238nffv 5735 . . . . . . . . . . . . . . 15
240236, 237, 239nfbr 4256 . . . . . . . . . . . . . 14
241 nfcv 2572 . . . . . . . . . . . . . . 15
242239, 237, 241nfbr 4256 . . . . . . . . . . . . . 14
243240, 242nfan 1846 . . . . . . . . . . . . 13
244235, 243nfral 2759 . . . . . . . . . . . 12
245 nfcv 2572 . . . . . . . . . . . . 13
246 nfcv 2572 . . . . . . . . . . . . . 14
247 nfcv 2572 . . . . . . . . . . . . . 14
248239, 246, 247nfbr 4256 . . . . . . . . . . . . 13
249245, 248nfral 2759 . . . . . . . . . . . 12
250 nfcv 2572 . . . . . . . . . . . . 13
251 nfcv 2572 . . . . . . . . . . . . . 14
252251, 246, 239nfbr 4256 . . . . . . . . . . . . 13
253250, 252nfral 2759 . . . . . . . . . . . 12
254244, 249, 253nf3an 1849 . . . . . . . . . . 11
255 nfcv 2572 . . . . . . . . . . . . . 14
256 nfcv 2572 . . . . . . . . . . . . . . . 16
257 nfcv 2572 . . . . . . . . . . . . . . . . . . 19
258 nfra1 2756 . . . . . . . . . . . . . . . . . . . . 21
259 nfra1 2756 . . . . . . . . . . . . . . . . . . . . 21
260 nfra1 2756 . . . . . . . . . . . . . . . . . . . . 21
261258, 259, 260nf3an 1849 . . . . . . . . . . . . . . . . . . . 20
262 nfcv 2572 . . . . . . . . . . . . . . . . . . . 20
263261, 262nfrab 2889 . . . . . . . . . . . . . . . . . . 19
264257, 263nfmpt 4297 . . . . . . . . . . . . . . . . . 18
2655, 264nfcxfr 2569 . . . . . . . . . . . . . . . . 17
266 nfcv 2572 . . . . . . . . . . . . . . . . 17
267265, 266nfco 5038 . . . . . . . . . . . . . . . 16
268256, 267nfco 5038 . . . . . . . . . . . . . . 15
269 nfcv 2572 . . . . . . . . . . . . . . 15
270268, 269nffv 5735 . . . . . . . . . . . . . 14
271255, 270nfeq 2579 . . . . . . . . . . . . 13
272 fveq1 5727 . . . . . . . . . . . . . . 15
273272breq2d 4224 . . . . . . . . . . . . . 14
274272breq1d 4222 . . . . . . . . . . . . . 14
275273, 274anbi12d 692 . . . . . . . . . . . . 13
276271, 275ralbid 2723 . . . . . . . . . . . 12
277272breq1d 4222 . . . . . . . . . . . . 13
278271, 277ralbid 2723 . . . . . . . . . . . 12
279272breq2d 4224 . . . . . . . . . . . . 13
280271, 279ralbid 2723 . . . . . . . . . . . 12
281276, 278, 2803anbi123d 1254 . . . . . . . . . . 11
282233, 234, 254, 281elrabf 3091 . . . . . . . . . 10
283282simprbi 451 . . . . . . . . 9
284283simp2d 970 . . . . . . . 8
285228, 284syl6bi 220 . . . . . . 7
286214, 285mpd 15 . . . . . 6
287 stoweidlem31.2 . . . . . . . . 9
288265nfrn 5112 . . . . . . . . . . 11
289256, 288nffn 5541 . . . . . . . . . 10
290 nfv 1629 . . . . . . . . . . 11
291288, 290nfral 2759 . . . . . . . . . 10
292289, 291nfan 1846 . . . . . . . . 9
293287, 292nfan 1846 . . . . . . . 8
294 nfv 1629 . . . . . . . 8
295293, 294nfan 1846 . . . . . . 7
296 stoweidlem31.11 . . . . . . . . . . 11
297296ad3antrrr 711 . . . . . . . . . 10
298 simpr 448 . . . . . . . . . 10
299297, 298sseldd 3349 . . . . . . . . 9
300283simp3d 971 . . . . . . . . . . . 12
301228, 300syl6bi 220 . . . . . . . . . . 11
302214, 301mpd 15 . . . . . . . . . 10
303302r19.21bi 2804 . . . . . . . . 9
304299, 303syldan 457 . . . . . . . 8
305304ex 424 . . . . . . 7
306295, 305ralrimi 2787 . . . . . 6
307286, 306jca 519 . . . . 5
308307ralrimiva 2789 . . . 4
309193, 308jca 519 . . 3
310 feq1 5576 . . . . 5
311 nfcv 2572 . . . . . . . . 9
312311, 268nfeq 2579 . . . . . . . 8
313 fveq1 5727 . . . . . . . . . 10
314313fveq1d 5730 . . . . . . . . 9
315314breq1d 4222 . . . . . . . 8
316312, 315ralbid 2723 . . . . . . 7
317314breq2d 4224 . . . . . . . 8
318312, 317ralbid 2723 . . . . . . 7
319316, 318anbi12d 692 . . . . . 6