Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkococnlem Structured version   Unicode version

Theorem xkococnlem 17691
 Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
xkococn.1
xkococn.s 𝑛Locally
xkococn.k
xkococn.c t
xkococn.v
xkococn.a
xkococn.b
xkococn.i
Assertion
Ref Expression
xkococnlem
Distinct variable groups:   ,   ,   ,,,,   ,,,   ,,   ,,,,   ,   ,,
Allowed substitution hints:   (,,,)   (,,)   (,,)   ()   (,,)   (,)   (,)

Proof of Theorem xkococnlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkococn.b . . . 4
2 xkococn.c . . . 4 t
3 imacmp 17460 . . . 4 t t
41, 2, 3syl2anc 643 . . 3 t
5 xkococn.s . . . . . . . . 9 𝑛Locally
65adantr 452 . . . . . . . 8 𝑛Locally
7 xkococn.a . . . . . . . . . 10
8 xkococn.v . . . . . . . . . 10
9 cnima 17329 . . . . . . . . . 10
107, 8, 9syl2anc 643 . . . . . . . . 9
1110adantr 452 . . . . . . . 8
12 imaco 5375 . . . . . . . . . . 11
13 xkococn.i . . . . . . . . . . 11
1412, 13syl5eqssr 3393 . . . . . . . . . 10
15 eqid 2436 . . . . . . . . . . . . 13
16 eqid 2436 . . . . . . . . . . . . 13
1715, 16cnf 17310 . . . . . . . . . . . 12
18 ffun 5593 . . . . . . . . . . . 12
197, 17, 183syl 19 . . . . . . . . . . 11
20 imassrn 5216 . . . . . . . . . . . . 13
21 eqid 2436 . . . . . . . . . . . . . . 15
2221, 15cnf 17310 . . . . . . . . . . . . . 14
23 frn 5597 . . . . . . . . . . . . . 14
241, 22, 233syl 19 . . . . . . . . . . . . 13
2520, 24syl5ss 3359 . . . . . . . . . . . 12
26 fdm 5595 . . . . . . . . . . . . 13
277, 17, 263syl 19 . . . . . . . . . . . 12
2825, 27sseqtr4d 3385 . . . . . . . . . . 11
29 funimass3 5846 . . . . . . . . . . 11
3019, 28, 29syl2anc 643 . . . . . . . . . 10
3114, 30mpbid 202 . . . . . . . . 9
3231sselda 3348 . . . . . . . 8
33 nlly2i 17539 . . . . . . . 8 𝑛Locally t
346, 11, 32, 33syl3anc 1184 . . . . . . 7 t
35 nllytop 17536 . . . . . . . . . . . . 13 𝑛Locally
365, 35syl 16 . . . . . . . . . . . 12
3736ad3antrrr 711 . . . . . . . . . . 11 t
38 imaexg 5217 . . . . . . . . . . . . 13
391, 38syl 16 . . . . . . . . . . . 12
4039ad3antrrr 711 . . . . . . . . . . 11 t
41 simprl 733 . . . . . . . . . . 11 t
42 elrestr 13656 . . . . . . . . . . 11 t
4337, 40, 41, 42syl3anc 1184 . . . . . . . . . 10 t t
44 simprr1 1005 . . . . . . . . . . 11 t
45 simpllr 736 . . . . . . . . . . 11 t
46 elin 3530 . . . . . . . . . . 11
4744, 45, 46sylanbrc 646 . . . . . . . . . 10 t
48 inss1 3561 . . . . . . . . . . . 12
49 elpwi 3807 . . . . . . . . . . . . . . 15
5049ad2antlr 708 . . . . . . . . . . . . . 14 t
51 elssuni 4043 . . . . . . . . . . . . . . . 16
5210, 51syl 16 . . . . . . . . . . . . . . 15
5352ad3antrrr 711 . . . . . . . . . . . . . 14 t
5450, 53sstrd 3358 . . . . . . . . . . . . 13 t
55 simprr2 1006 . . . . . . . . . . . . 13 t
5615ssntr 17122 . . . . . . . . . . . . 13
5737, 54, 41, 55, 56syl22anc 1185 . . . . . . . . . . . 12 t
5848, 57syl5ss 3359 . . . . . . . . . . 11 t
59 simprr3 1007 . . . . . . . . . . 11 t t
6058, 59jca 519 . . . . . . . . . 10 t t
61 eleq2 2497 . . . . . . . . . . . 12
62 sseq1 3369 . . . . . . . . . . . . 13
6362anbi1d 686 . . . . . . . . . . . 12 t t
6461, 63anbi12d 692 . . . . . . . . . . 11 t t
6564rspcev 3052 . . . . . . . . . 10 t t t t
6643, 47, 60, 65syl12anc 1182 . . . . . . . . 9 t t t
6766rexlimdvaa 2831 . . . . . . . 8 t t t
6867reximdva 2818 . . . . . . 7 t t t
6934, 68mpd 15 . . . . . 6 t t
70 rexcom 2869 . . . . . . 7 t t t t
71 r19.42v 2862 . . . . . . . 8 t t
7271rexbii 2730 . . . . . . 7 t t t t
7370, 72bitri 241 . . . . . 6 t t t t
7469, 73sylib 189 . . . . 5 t t
7574ralrimiva 2789 . . . 4 t t
7615restuni 17226 . . . . . 6 t
7736, 25, 76syl2anc 643 . . . . 5 t
7877raleqdv 2910 . . . 4 t t t t t
7975, 78mpbid 202 . . 3 t t t
80 eqid 2436 . . . 4 t t
81 fveq2 5728 . . . . . 6
8281sseq2d 3376 . . . . 5
83 oveq2 6089 . . . . . 6 t t
8483eleq1d 2502 . . . . 5 t t
8582, 84anbi12d 692 . . . 4 t t
8680, 85cmpcovf 17454 . . 3 t t t t t t t
874, 79, 86syl2anc 643 . 2 t t t
8877adantr 452 . . . . . . 7 t t
8988eqeq1d 2444 . . . . . 6 t t
9089biimpar 472 . . . . 5 t t
9136ad2antrr 707 . . . . . . . . . 10 t t
92 cntop2 17305 . . . . . . . . . . . 12
937, 92syl 16 . . . . . . . . . . 11
9493ad2antrr 707 . . . . . . . . . 10 t t
95 xkotop 17620 . . . . . . . . . 10
9691, 94, 95syl2anc 643 . . . . . . . . 9 t t
97 cntop1 17304 . . . . . . . . . . . 12
981, 97syl 16 . . . . . . . . . . 11
9998ad2antrr 707 . . . . . . . . . 10 t t
100 xkotop 17620 . . . . . . . . . 10
10199, 91, 100syl2anc 643 . . . . . . . . 9 t t
102 simprrl 741 . . . . . . . . . . . . 13 t t
103 frn 5597 . . . . . . . . . . . . 13
104102, 103syl 16 . . . . . . . . . . . 12 t t
105 sspwuni 4176 . . . . . . . . . . . 12
106104, 105sylib 189 . . . . . . . . . . 11 t t
10710ad2antrr 707 . . . . . . . . . . . 12 t t
108107, 51syl 16 . . . . . . . . . . 11 t t
109106, 108sstrd 3358 . . . . . . . . . 10 t t
110 ffn 5591 . . . . . . . . . . . . 13
111 fniunfv 5994 . . . . . . . . . . . . 13
112102, 110, 1113syl 19 . . . . . . . . . . . 12 t t
113112oveq2d 6097 . . . . . . . . . . 11 t t t t
114 inss2 3562 . . . . . . . . . . . . 13 t
115 simplr 732 . . . . . . . . . . . . 13 t t t
116114, 115sseldi 3346 . . . . . . . . . . . 12 t t
117 simprrr 742 . . . . . . . . . . . . 13 t t t
118 simpr 448 . . . . . . . . . . . . . 14 t t
119118ralimi 2781 . . . . . . . . . . . . 13 t t
120117, 119syl 16 . . . . . . . . . . . 12 t t t
12115fiuncmp 17467 . . . . . . . . . . . 12 t t
12291, 116, 120, 121syl3anc 1184 . . . . . . . . . . 11 t t t
123113, 122eqeltrrd 2511 . . . . . . . . . 10 t t t
1248ad2antrr 707 . . . . . . . . . 10 t t
12515, 91, 94, 109, 123, 124xkoopn 17621 . . . . . . . . 9 t t
126 xkococn.k . . . . . . . . . . 11
127126ad2antrr 707 . . . . . . . . . 10 t t
1282ad2antrr 707 . . . . . . . . . 10 t t t
129112, 109eqsstrd 3382 . . . . . . . . . . . . 13 t t
130 iunss 4132 . . . . . . . . . . . . 13
131129, 130sylib 189 . . . . . . . . . . . 12 t t
13215ntropn 17113 . . . . . . . . . . . . . 14
133132ex 424 . . . . . . . . . . . . 13
134133ralimdv 2785 . . . . . . . . . . . 12
13591, 131, 134sylc 58 . . . . . . . . . . 11 t t
136 iunopn 16971 . . . . . . . . . . 11
13791, 135, 136syl2anc 643 . . . . . . . . . 10 t t
13821, 99, 91, 127, 128, 137xkoopn 17621 . . . . . . . . 9 t t
139 txopn 17634 . . . . . . . . 9
14096, 101, 125, 138, 139syl22anc 1185 . . . . . . . 8 t t
1417ad2antrr 707 . . . . . . . . . 10 t t
142 imaiun 5992 . . . . . . . . . . . 12
143112imaeq2d 5203 . . . . . . . . . . . 12 t t
144142, 143syl5eqr 2482 . . . . . . . . . . 11 t t
145112, 106eqsstrd 3382 . . . . . . . . . . . 12 t t
14619ad2antrr 707 . . . . . . . . . . . . 13 t t
147102, 110syl 16 . . . . . . . . . . . . 13 t t
14827ad2antrr 707 . . . . . . . . . . . . . 14 t t
149109, 148sseqtr4d 3385 . . . . . . . . . . . . 13 t t
150 simpl1 960 . . . . . . . . . . . . . . . 16
1511113ad2ant2 979 . . . . . . . . . . . . . . . . . . 19
152 simp3 959 . . . . . . . . . . . . . . . . . . 19
153151, 152eqsstrd 3382 . . . . . . . . . . . . . . . . . 18
154 iunss 4132 . . . . . . . . . . . . . . . . . 18
155153, 154sylib 189 . . . . . . . . . . . . . . . . 17
156155r19.21bi 2804 . . . . . . . . . . . . . . . 16
157 funimass3 5846 . . . . . . . . . . . . . . . 16
158150, 156, 157syl2anc 643 . . . . . . . . . . . . . . 15
159158ralbidva 2721 . . . . . . . . . . . . . 14
160 iunss 4132 . . . . . . . . . . . . . 14
161 iunss 4132 . . . . . . . . . . . . . 14
162159, 160, 1613bitr4g 280 . . . . . . . . . . . . 13
163146, 147, 149, 162syl3anc 1184 . . . . . . . . . . . 12 t t
164145, 163mpbird 224 . . . . . . . . . . 11 t t
165144, 164eqsstr3d 3383 . . . . . . . . . 10 t t
166 imaeq1 5198 . . . . . . . . . . . 12
167166sseq1d 3375 . . . . . . . . . . 11
168167elrab 3092 . . . . . . . . . 10
169141, 165, 168sylanbrc 646 . . . . . . . . 9 t t
1701ad2antrr 707 . . . . . . . . . 10 t t
171 simprl 733 . . . . . . . . . . . 12 t t
172 uniiun 4144 . . . . . . . . . . . 12
173171, 172syl6eq 2484 . . . . . . . . . . 11 t t
174 simpl 444 . . . . . . . . . . . . 13 t
175174ralimi 2781 . . . . . . . . . . . 12 t
176 ss2iun 4108 . . . . . . . . . . . 12
177117, 175, 1763syl 19 . . . . . . . . . . 11 t t
178173, 177eqsstrd 3382 . . . . . . . . . 10 t t
179 imaeq1 5198 . . . . . . . . . . . 12
180179sseq1d 3375 . . . . . . . . . . 11
181180elrab 3092 . . . . . . . . . 10
182170, 178, 181sylanbrc 646 . . . . . . . . 9 t t
183 opelxpi 4910 . . . . . . . . 9
184169, 182, 183syl2anc 643 . . . . . . . 8 t t
185 imaeq1 5198 . . . . . . . . . . . . . . 15
186185sseq1d 3375 . . . . . . . . . . . . . 14
187186elrab 3092 . . . . . . . . . . . . 13
188 imaeq1 5198 . . . . . . . . . . . . . . 15
189188sseq1d 3375 . . . . . . . . . . . . . 14
190189elrab 3092 . . . . . . . . . . . . 13
191187, 190anbi12i 679 . . . . . . . . . . . 12
192 simprll 739 . . . . . . . . . . . . . 14 t t
193 simprrl 741 . . . . . . . . . . . . . 14 t t
194 coeq1 5030 . . . . . . . . . . . . . . 15
195 coeq2 5031 . . . . . . . . . . . . . . 15
196 xkococn.1 . . . . . . . . . . . . . . 15
197 vex 2959 . . . . . . . . . . . . . . . 16
198 vex 2959 . . . . . . . . . . . . . . . 16
199197, 198coex 5413 . . . . . . . . . . . . . . 15
200194, 195, 196, 199ovmpt2 6209 . . . . . . . . . . . . . 14
201192, 193, 200syl2anc 643 . . . . . . . . . . . . 13 t t
202 cnco 17330 . . . . . . . . . . . . . . 15
203193, 192, 202syl2anc 643 . . . . . . . . . . . . . 14 t t
204 imaco 5375 . . . . . . . . . . . . . . 15
205 simprrr 742 . . . . . . . . . . . . . . . . . 18 t t
20615ntrss2 17121 . . . . . . . . . . . . . . . . . . . . . . . 24
207206ex 424 . . . . . . . . . . . . . . . . . . . . . . 23
208207ralimdv 2785 . . . . . . . . . . . . . . . . . . . . . 22
20991, 131, 208sylc 58 . . . . . . . . . . . . . . . . . . . . 21 t t
210 ss2iun 4108 . . . . . . . . . . . . . . . . . . . . 21
211209, 210syl 16 . . . . . . . . . . . . . . . . . . . 20 t t
212211, 112sseqtrd 3384 . . . . . . . . . . . . . . . . . . 19 t t
213212adantr 452 . . . . . . . . . . . . . . . . . 18 t t
214205, 213sstrd 3358 . . . . . . . . . . . . . . . . 17 t t
215 imass2 5240 . . . . . . . . . . . . . . . . 17
216214, 215syl 16 . . . . . . . . . . . . . . . 16 t t
217 simprlr 740 . . . . . . . . . . . . . . . 16 t t
218216, 217sstrd 3358 . . . . . . . . . . . . . . 15 t t
219204, 218syl5eqss 3392 . . . . . . . . . . . . . 14 t t
220 imaeq1 5198 . . . . . . . . . . . . . . . 16
221220sseq1d 3375 . . . . . . . . . . . . . . 15
222221elrab 3092 . . . . . . . . . . . . . 14
223203, 219, 222sylanbrc 646 . . . . . . . . . . . . 13 t t
224201, 223eqeltrd 2510 . . . . . . . . . . . 12 t t
225191, 224sylan2b 462 . . . . . . . . . . 11 t t
226225ralrimivva 2798 . . . . . . . . . 10 t t
227196mpt2fun 6172 . . . . . . . . . . 11
228 ssrab2 3428 . . . . . . . . . . . . 13
229 ssrab2 3428 . . . . . . . . . . . . 13
230 xpss12 4981 . . . . . . . . . . . . 13
231228, 229, 230mp2an 654 . . . . . . . . . . . 12
232 vex 2959 . . . . . . . . . . . . . 14
233 vex 2959 . . . . . . . . . . . . . 14
234232, 233coex 5413 . . . . . . . . . . . . 13
235196, 234dmmpt2 6421 . . . . . . . . . . . 12
236231, 235sseqtr4i 3381 . . . . . . . . . . 11
237 funimassov 6223 . . . . . . . . . . 11
238227, 236, 237mp2an 654 . . . . . . . . . 10
239226, 238sylibr 204 . . . . . . . . 9 t t
240 funimass3 5846 . . . . . . . . . 10
241227, 236, 240mp2an 654 . . . . . . . . 9
242239, 241sylib 189 . . . . . . . 8 t t
243 eleq2 2497 . . . . . . . . . 10
244 sseq1 3369 . . . . . . . . . 10
245243, 244anbi12d 692 . . . . . . . . 9
246245rspcev 3052 . . . . . . . 8
247140, 184, 242, 246syl12anc 1182 . . . . . . 7 t t
248247expr 599 . . . . . 6 t t
249248exlimdv 1646 . . . . 5 t