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

Theorem kgencn3 20566
 Description: The set of continuous functions from to is unaffected by k-ification of , if is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
kgencn3 𝑘Gen 𝑘Gen

Proof of Theorem kgencn3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2450 . . . . . . 7
2 eqid 2450 . . . . . . 7
31, 2cnf 20255 . . . . . 6
43adantl 468 . . . . 5 𝑘Gen
5 cnvimass 5187 . . . . . . . . 9
6 fdm 5731 . . . . . . . . . . 11
74, 6syl 17 . . . . . . . . . 10 𝑘Gen
87adantr 467 . . . . . . . . 9 𝑘Gen 𝑘Gen
95, 8syl5sseq 3479 . . . . . . . 8 𝑘Gen 𝑘Gen
10 cnvresima 5323 . . . . . . . . . . . 12
114ad2antrr 731 . . . . . . . . . . . . . . 15 𝑘Gen 𝑘Gen t
12 ffun 5729 . . . . . . . . . . . . . . 15
13 inpreima 6005 . . . . . . . . . . . . . . 15
1411, 12, 133syl 18 . . . . . . . . . . . . . 14 𝑘Gen 𝑘Gen t
1514ineq1d 3632 . . . . . . . . . . . . 13 𝑘Gen 𝑘Gen t
16 in32 3643 . . . . . . . . . . . . . 14
17 ssrin 3656 . . . . . . . . . . . . . . . . . 18
185, 17ax-mp 5 . . . . . . . . . . . . . . . . 17
19 dminss 5249 . . . . . . . . . . . . . . . . 17
2018, 19sstri 3440 . . . . . . . . . . . . . . . 16
2120a1i 11 . . . . . . . . . . . . . . 15 𝑘Gen 𝑘Gen t
22 df-ss 3417 . . . . . . . . . . . . . . 15
2321, 22sylib 200 . . . . . . . . . . . . . 14 𝑘Gen 𝑘Gen t
2416, 23syl5eq 2496 . . . . . . . . . . . . 13 𝑘Gen 𝑘Gen t
2515, 24eqtrd 2484 . . . . . . . . . . . 12 𝑘Gen 𝑘Gen t
2610, 25syl5eq 2496 . . . . . . . . . . 11 𝑘Gen 𝑘Gen t
27 simpr 463 . . . . . . . . . . . . . . 15 𝑘Gen
2827ad2antrr 731 . . . . . . . . . . . . . 14 𝑘Gen 𝑘Gen t
29 elpwi 3959 . . . . . . . . . . . . . . 15
3029ad2antrl 733 . . . . . . . . . . . . . 14 𝑘Gen 𝑘Gen t
311cnrest 20294 . . . . . . . . . . . . . 14 t
3228, 30, 31syl2anc 666 . . . . . . . . . . . . 13 𝑘Gen 𝑘Gen t t
33 simpr 463 . . . . . . . . . . . . . . . 16 𝑘Gen
3433ad3antrrr 735 . . . . . . . . . . . . . . 15 𝑘Gen 𝑘Gen t
352toptopon 19941 . . . . . . . . . . . . . . 15 TopOn
3634, 35sylib 200 . . . . . . . . . . . . . 14 𝑘Gen 𝑘Gen t TopOn
37 df-ima 4846 . . . . . . . . . . . . . . . 16
3837eqimss2i 3486 . . . . . . . . . . . . . . 15
3938a1i 11 . . . . . . . . . . . . . 14 𝑘Gen 𝑘Gen t
40 imassrn 5178 . . . . . . . . . . . . . . 15
41 frn 5733 . . . . . . . . . . . . . . . 16
4211, 41syl 17 . . . . . . . . . . . . . . 15 𝑘Gen 𝑘Gen t
4340, 42syl5ss 3442 . . . . . . . . . . . . . 14 𝑘Gen 𝑘Gen t
44 cnrest2 20295 . . . . . . . . . . . . . 14 TopOn t t t
4536, 39, 43, 44syl3anc 1267 . . . . . . . . . . . . 13 𝑘Gen 𝑘Gen t t t t
4632, 45mpbid 214 . . . . . . . . . . . 12 𝑘Gen 𝑘Gen t t t
47 simplr 761 . . . . . . . . . . . . 13 𝑘Gen 𝑘Gen t 𝑘Gen
48 simprr 765 . . . . . . . . . . . . . 14 𝑘Gen 𝑘Gen t t
49 imacmp 20405 . . . . . . . . . . . . . 14 t t
5028, 48, 49syl2anc 666 . . . . . . . . . . . . 13 𝑘Gen 𝑘Gen t t
51 kgeni 20545 . . . . . . . . . . . . 13 𝑘Gen t t
5247, 50, 51syl2anc 666 . . . . . . . . . . . 12 𝑘Gen 𝑘Gen t t
53 cnima 20274 . . . . . . . . . . . 12 t t t t
5446, 52, 53syl2anc 666 . . . . . . . . . . 11 𝑘Gen 𝑘Gen t t
5526, 54eqeltrrd 2529 . . . . . . . . . 10 𝑘Gen 𝑘Gen t t
5655expr 619 . . . . . . . . 9 𝑘Gen 𝑘Gen t t
5756ralrimiva 2801 . . . . . . . 8 𝑘Gen 𝑘Gen t t
58 kgentop 20550 . . . . . . . . . . 11 𝑘Gen
5958ad3antrrr 735 . . . . . . . . . 10 𝑘Gen 𝑘Gen
601toptopon 19941 . . . . . . . . . 10 TopOn
6159, 60sylib 200 . . . . . . . . 9 𝑘Gen 𝑘Gen TopOn
62 elkgen 20544 . . . . . . . . 9 TopOn 𝑘Gen t t
6361, 62syl 17 . . . . . . . 8 𝑘Gen 𝑘Gen 𝑘Gen t t
649, 57, 63mpbir2and 932 . . . . . . 7 𝑘Gen 𝑘Gen 𝑘Gen
65 kgenidm 20555 . . . . . . . 8 𝑘Gen 𝑘Gen
6665ad3antrrr 735 . . . . . . 7 𝑘Gen 𝑘Gen 𝑘Gen
6764, 66eleqtrd 2530 . . . . . 6 𝑘Gen 𝑘Gen
6867ralrimiva 2801 . . . . 5 𝑘Gen 𝑘Gen
6958, 60sylib 200 . . . . . . 7 𝑘Gen TopOn
70 kgentopon 20546 . . . . . . . 8 TopOn 𝑘Gen TopOn
7135, 70sylbi 199 . . . . . . 7 𝑘Gen TopOn
72 iscn 20244 . . . . . . 7 TopOn 𝑘Gen TopOn 𝑘Gen 𝑘Gen
7369, 71, 72syl2an 480 . . . . . 6 𝑘Gen 𝑘Gen 𝑘Gen
7473adantr 467 . . . . 5 𝑘Gen 𝑘Gen 𝑘Gen
754, 68, 74mpbir2and 932 . . . 4 𝑘Gen 𝑘Gen
7675ex 436 . . 3 𝑘Gen 𝑘Gen
7776ssrdv 3437 . 2 𝑘Gen 𝑘Gen
7871adantl 468 . . . 4 𝑘Gen 𝑘Gen TopOn
79 toponcom 19938 . . . 4 𝑘Gen TopOn TopOn𝑘Gen
8033, 78, 79syl2anc 666 . . 3 𝑘Gen TopOn𝑘Gen
81 kgenss 20551 . . . 4 𝑘Gen
8281adantl 468 . . 3 𝑘Gen 𝑘Gen
83 eqid 2450 . . . 4 𝑘Gen 𝑘Gen
8483cnss2 20286 . . 3 TopOn𝑘Gen 𝑘Gen 𝑘Gen
8580, 82, 84syl2anc 666 . 2 𝑘Gen 𝑘Gen
8677, 85eqssd 3448 1 𝑘Gen 𝑘Gen
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1443   wcel 1886  wral 2736   cin 3402   wss 3403  cpw 3950  cuni 4197  ccnv 4832   cdm 4833   crn 4834   cres 4835  cima 4836   wfun 5575  wf 5577  cfv 5581  (class class class)co 6288   ↾t crest 15312  ctop 19910  TopOnctopon 19911   ccn 20233  ccmp 20394  𝑘Genckgen 20541 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-oadd 7183  df-er 7360  df-map 7471  df-en 7567  df-dom 7568  df-fin 7570  df-fi 7922  df-rest 15314  df-topgen 15335  df-top 19914  df-bases 19915  df-topon 19916  df-cn 20236  df-cmp 20395  df-kgen 20542 This theorem is referenced by:  kgen2cn  20567  txkgen  20660  qtopkgen  20718
 Copyright terms: Public domain W3C validator