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

Theorem xkococnlem 20605
 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 20343 . . . 4 t t
41, 2, 3syl2anc 665 . . 3 t
5 xkococn.s . . . . . . . . 9 𝑛Locally
65adantr 466 . . . . . . . 8 𝑛Locally
7 xkococn.a . . . . . . . . . 10
8 xkococn.v . . . . . . . . . 10
9 cnima 20212 . . . . . . . . . 10
107, 8, 9syl2anc 665 . . . . . . . . 9
1110adantr 466 . . . . . . . 8
12 imaco 5360 . . . . . . . . . . 11
13 xkococn.i . . . . . . . . . . 11
1412, 13syl5eqssr 3515 . . . . . . . . . 10
15 eqid 2429 . . . . . . . . . . . . 13
16 eqid 2429 . . . . . . . . . . . . 13
1715, 16cnf 20193 . . . . . . . . . . . 12
18 ffun 5748 . . . . . . . . . . . 12
197, 17, 183syl 18 . . . . . . . . . . 11
20 imassrn 5199 . . . . . . . . . . . . 13
21 eqid 2429 . . . . . . . . . . . . . . 15
2221, 15cnf 20193 . . . . . . . . . . . . . 14
23 frn 5752 . . . . . . . . . . . . . 14
241, 22, 233syl 18 . . . . . . . . . . . . 13
2520, 24syl5ss 3481 . . . . . . . . . . . 12
26 fdm 5750 . . . . . . . . . . . . 13
277, 17, 263syl 18 . . . . . . . . . . . 12
2825, 27sseqtr4d 3507 . . . . . . . . . . 11
29 funimass3 6013 . . . . . . . . . . 11
3019, 28, 29syl2anc 665 . . . . . . . . . 10
3114, 30mpbid 213 . . . . . . . . 9
3231sselda 3470 . . . . . . . 8
33 nlly2i 20422 . . . . . . . 8 𝑛Locally t
346, 11, 32, 33syl3anc 1264 . . . . . . 7 t
35 nllytop 20419 . . . . . . . . . . . . 13 𝑛Locally
365, 35syl 17 . . . . . . . . . . . 12
3736ad3antrrr 734 . . . . . . . . . . 11 t
38 imaexg 6744 . . . . . . . . . . . . 13
391, 38syl 17 . . . . . . . . . . . 12
4039ad3antrrr 734 . . . . . . . . . . 11 t
41 simprl 762 . . . . . . . . . . 11 t
42 elrestr 15286 . . . . . . . . . . 11 t
4337, 40, 41, 42syl3anc 1264 . . . . . . . . . 10 t t
44 simprr1 1053 . . . . . . . . . . 11 t
45 simpllr 767 . . . . . . . . . . 11 t
4644, 45elind 3656 . . . . . . . . . 10 t
47 inss1 3688 . . . . . . . . . . . 12
48 elpwi 3994 . . . . . . . . . . . . . . 15
4948ad2antlr 731 . . . . . . . . . . . . . 14 t
50 elssuni 4251 . . . . . . . . . . . . . . . 16
5110, 50syl 17 . . . . . . . . . . . . . . 15
5251ad3antrrr 734 . . . . . . . . . . . . . 14 t
5349, 52sstrd 3480 . . . . . . . . . . . . 13 t
54 simprr2 1054 . . . . . . . . . . . . 13 t
5515ssntr 20004 . . . . . . . . . . . . 13
5637, 53, 41, 54, 55syl22anc 1265 . . . . . . . . . . . 12 t
5747, 56syl5ss 3481 . . . . . . . . . . 11 t
58 simprr3 1055 . . . . . . . . . . 11 t t
5957, 58jca 534 . . . . . . . . . 10 t t
60 eleq2 2502 . . . . . . . . . . . 12
61 sseq1 3491 . . . . . . . . . . . . 13
6261anbi1d 709 . . . . . . . . . . . 12 t t
6360, 62anbi12d 715 . . . . . . . . . . 11 t t
6463rspcev 3188 . . . . . . . . . 10 t t t t
6543, 46, 59, 64syl12anc 1262 . . . . . . . . 9 t t t
6665rexlimdvaa 2925 . . . . . . . 8 t t t
6766reximdva 2907 . . . . . . 7 t t t
6834, 67mpd 15 . . . . . 6 t t
69 rexcom 2997 . . . . . . 7 t t t t
70 r19.42v 2990 . . . . . . . 8 t t
7170rexbii 2934 . . . . . . 7 t t t t
7269, 71bitri 252 . . . . . 6 t t t t
7368, 72sylib 199 . . . . 5 t t
7473ralrimiva 2846 . . . 4 t t
7515restuni 20109 . . . . . 6 t
7636, 25, 75syl2anc 665 . . . . 5 t
7776raleqdv 3038 . . . 4 t t t t t
7874, 77mpbid 213 . . 3 t t t
79 eqid 2429 . . . 4 t t
80 fveq2 5881 . . . . . 6
8180sseq2d 3498 . . . . 5
82 oveq2 6313 . . . . . 6 t t
8382eleq1d 2498 . . . . 5 t t
8481, 83anbi12d 715 . . . 4 t t
8579, 84cmpcovf 20337 . . 3 t t t t t t t
864, 78, 85syl2anc 665 . 2 t t t
8776adantr 466 . . . . . . 7 t t
8887eqeq1d 2431 . . . . . 6 t t
8988biimpar 487 . . . . 5 t t
9036ad2antrr 730 . . . . . . . . . 10 t t
91 cntop2 20188 . . . . . . . . . . . 12
927, 91syl 17 . . . . . . . . . . 11
9392ad2antrr 730 . . . . . . . . . 10 t t
94 xkotop 20534 . . . . . . . . . 10
9590, 93, 94syl2anc 665 . . . . . . . . 9 t t
96 cntop1 20187 . . . . . . . . . . . 12
971, 96syl 17 . . . . . . . . . . 11
9897ad2antrr 730 . . . . . . . . . 10 t t
99 xkotop 20534 . . . . . . . . . 10
10098, 90, 99syl2anc 665 . . . . . . . . 9 t t
101 simprrl 772 . . . . . . . . . . . . 13 t t
102 frn 5752 . . . . . . . . . . . . 13
103101, 102syl 17 . . . . . . . . . . . 12 t t
104 sspwuni 4391 . . . . . . . . . . . 12
105103, 104sylib 199 . . . . . . . . . . 11 t t
10610ad2antrr 730 . . . . . . . . . . . 12 t t
107106, 50syl 17 . . . . . . . . . . 11 t t
108105, 107sstrd 3480 . . . . . . . . . 10 t t
109 ffn 5746 . . . . . . . . . . . . 13
110 fniunfv 6167 . . . . . . . . . . . . 13
111101, 109, 1103syl 18 . . . . . . . . . . . 12 t t
112111oveq2d 6321 . . . . . . . . . . 11 t t t t
113 inss2 3689 . . . . . . . . . . . . 13 t
114 simplr 760 . . . . . . . . . . . . 13 t t t
115113, 114sseldi 3468 . . . . . . . . . . . 12 t t
116 simprrr 773 . . . . . . . . . . . . 13 t t t
117 simpr 462 . . . . . . . . . . . . . 14 t t
118117ralimi 2825 . . . . . . . . . . . . 13 t t
119116, 118syl 17 . . . . . . . . . . . 12 t t t
12015fiuncmp 20350 . . . . . . . . . . . 12 t t
12190, 115, 119, 120syl3anc 1264 . . . . . . . . . . 11 t t t
122112, 121eqeltrrd 2518 . . . . . . . . . 10 t t t
1238ad2antrr 730 . . . . . . . . . 10 t t
12415, 90, 93, 108, 122, 123xkoopn 20535 . . . . . . . . 9 t t
125 xkococn.k . . . . . . . . . . 11
126125ad2antrr 730 . . . . . . . . . 10 t t
1272ad2antrr 730 . . . . . . . . . 10 t t t
128111, 108eqsstrd 3504 . . . . . . . . . . . . 13 t t
129 iunss 4343 . . . . . . . . . . . . 13
130128, 129sylib 199 . . . . . . . . . . . 12 t t
13115ntropn 19995 . . . . . . . . . . . . . 14
132131ex 435 . . . . . . . . . . . . 13
133132ralimdv 2842 . . . . . . . . . . . 12
13490, 130, 133sylc 62 . . . . . . . . . . 11 t t
135 iunopn 19859 . . . . . . . . . . 11
13690, 134, 135syl2anc 665 . . . . . . . . . 10 t t
13721, 98, 90, 126, 127, 136xkoopn 20535 . . . . . . . . 9 t t
138 txopn 20548 . . . . . . . . 9
13995, 100, 124, 137, 138syl22anc 1265 . . . . . . . 8 t t
1407ad2antrr 730 . . . . . . . . . 10 t t
141 imaiun 6165 . . . . . . . . . . . 12
142111imaeq2d 5188 . . . . . . . . . . . 12 t t
143141, 142syl5eqr 2484 . . . . . . . . . . 11 t t
144111, 105eqsstrd 3504 . . . . . . . . . . . 12 t t
14519ad2antrr 730 . . . . . . . . . . . . 13 t t
146101, 109syl 17 . . . . . . . . . . . . 13 t t
14727ad2antrr 730 . . . . . . . . . . . . . 14 t t
148108, 147sseqtr4d 3507 . . . . . . . . . . . . 13 t t
149 simpl1 1008 . . . . . . . . . . . . . . . 16
1501103ad2ant2 1027 . . . . . . . . . . . . . . . . . . 19
151 simp3 1007 . . . . . . . . . . . . . . . . . . 19
152150, 151eqsstrd 3504 . . . . . . . . . . . . . . . . . 18
153 iunss 4343 . . . . . . . . . . . . . . . . . 18
154152, 153sylib 199 . . . . . . . . . . . . . . . . 17
155154r19.21bi 2801 . . . . . . . . . . . . . . . 16
156 funimass3 6013 . . . . . . . . . . . . . . . 16
157149, 155, 156syl2anc 665 . . . . . . . . . . . . . . 15
158157ralbidva 2868 . . . . . . . . . . . . . 14
159 iunss 4343 . . . . . . . . . . . . . 14
160 iunss 4343 . . . . . . . . . . . . . 14
161158, 159, 1603bitr4g 291 . . . . . . . . . . . . 13
162145, 146, 148, 161syl3anc 1264 . . . . . . . . . . . 12 t t
163144, 162mpbird 235 . . . . . . . . . . 11 t t
164143, 163eqsstr3d 3505 . . . . . . . . . 10 t t
165 imaeq1 5183 . . . . . . . . . . . 12
166165sseq1d 3497 . . . . . . . . . . 11
167166elrab 3235 . . . . . . . . . 10
168140, 164, 167sylanbrc 668 . . . . . . . . 9 t t
1691ad2antrr 730 . . . . . . . . . 10 t t
170 simprl 762 . . . . . . . . . . . 12 t t
171 uniiun 4355 . . . . . . . . . . . 12
172170, 171syl6eq 2486 . . . . . . . . . . 11 t t
173 simpl 458 . . . . . . . . . . . . 13 t
174173ralimi 2825 . . . . . . . . . . . 12 t
175 ss2iun 4318 . . . . . . . . . . . 12
176116, 174, 1753syl 18 . . . . . . . . . . 11 t t
177172, 176eqsstrd 3504 . . . . . . . . . 10 t t
178 imaeq1 5183 . . . . . . . . . . . 12
179178sseq1d 3497 . . . . . . . . . . 11
180179elrab 3235 . . . . . . . . . 10
181169, 177, 180sylanbrc 668 . . . . . . . . 9 t t
182 opelxpi 4886 . . . . . . . . 9
183168, 181, 182syl2anc 665 . . . . . . . 8 t t
184 imaeq1 5183 . . . . . . . . . . . . . . 15
185184sseq1d 3497 . . . . . . . . . . . . . 14
186185elrab 3235 . . . . . . . . . . . . 13
187 imaeq1 5183 . . . . . . . . . . . . . . 15
188187sseq1d 3497 . . . . . . . . . . . . . 14
189188elrab 3235 . . . . . . . . . . . . 13
190186, 189anbi12i 701 . . . . . . . . . . . 12
191 simprll 770 . . . . . . . . . . . . . 14 t t
192 simprrl 772 . . . . . . . . . . . . . 14 t t
193 coeq1 5012 . . . . . . . . . . . . . . 15
194 coeq2 5013 . . . . . . . . . . . . . . 15
195 xkococn.1 . . . . . . . . . . . . . . 15
196 vex 3090 . . . . . . . . . . . . . . . 16
197 vex 3090 . . . . . . . . . . . . . . . 16
198196, 197coex 6759 . . . . . . . . . . . . . . 15
199193, 194, 195, 198ovmpt2 6446 . . . . . . . . . . . . . 14
200191, 192, 199syl2anc 665 . . . . . . . . . . . . 13 t t
201 cnco 20213 . . . . . . . . . . . . . . 15
202192, 191, 201syl2anc 665 . . . . . . . . . . . . . 14 t t
203 imaco 5360 . . . . . . . . . . . . . . 15
204 simprrr 773 . . . . . . . . . . . . . . . . . 18 t t
20515ntrss2 20003 . . . . . . . . . . . . . . . . . . . . . . . 24
206205ex 435 . . . . . . . . . . . . . . . . . . . . . . 23
207206ralimdv 2842 . . . . . . . . . . . . . . . . . . . . . 22
20890, 130, 207sylc 62 . . . . . . . . . . . . . . . . . . . . 21 t t
209 ss2iun 4318 . . . . . . . . . . . . . . . . . . . . 21
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . 20 t t
211210, 111sseqtrd 3506 . . . . . . . . . . . . . . . . . . 19 t t
212211adantr 466 . . . . . . . . . . . . . . . . . 18 t t
213204, 212sstrd 3480 . . . . . . . . . . . . . . . . 17 t t
214 imass2 5224 . . . . . . . . . . . . . . . . 17
215213, 214syl 17 . . . . . . . . . . . . . . . 16 t t
216 simprlr 771 . . . . . . . . . . . . . . . 16 t t
217215, 216sstrd 3480 . . . . . . . . . . . . . . 15 t t
218203, 217syl5eqss 3514 . . . . . . . . . . . . . 14 t t
219 imaeq1 5183 . . . . . . . . . . . . . . . 16
220219sseq1d 3497 . . . . . . . . . . . . . . 15
221220elrab 3235 . . . . . . . . . . . . . 14
222202, 218, 221sylanbrc 668 . . . . . . . . . . . . 13 t t
223200, 222eqeltrd 2517 . . . . . . . . . . . 12 t t
224190, 223sylan2b 477 . . . . . . . . . . 11 t t
225224ralrimivva 2853 . . . . . . . . . 10 t t
226195mpt2fun 6412 . . . . . . . . . . 11
227 ssrab2 3552 . . . . . . . . . . . . 13
228 ssrab2 3552 . . . . . . . . . . . . 13
229 xpss12 4960 . . . . . . . . . . . . 13
230227, 228, 229mp2an 676 . . . . . . . . . . . 12
231 vex 3090 . . . . . . . . . . . . . 14
232 vex 3090 . . . . . . . . . . . . . 14
233231, 232coex 6759 . . . . . . . . . . . . 13
234195, 233dmmpt2 6877 . . . . . . . . . . . 12
235230, 234sseqtr4i 3503 . . . . . . . . . . 11
236 funimassov 6460 . . . . . . . . . . 11
237226, 235, 236mp2an 676 . . . . . . . . . 10
238225, 237sylibr 215 . . . . . . . . 9 t t
239 funimass3 6013 . . . . . . . . . 10
240226, 235, 239mp2an 676 . . . . . . . . 9
241238, 240sylib 199 . . . . . . . 8 t t
242 eleq2 2502 . . . . . . . . . 10
243 sseq1 3491 . . . . . . . . . 10
244242, 243anbi12d 715 . . . . . . . . 9
245244rspcev 3188 . . . . . . . 8
246139, 183, 241, 245syl12anc 1262 . . . . . . 7 t t
247246expr 618 . . . . . 6 t t
248247exlimdv 1771 . . . . 5 t t