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

Theorem fmucnd 21294
 Description: The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017.)
Hypotheses
Ref Expression
fmucnd.1 UnifOn
fmucnd.2 UnifOn
fmucnd.3 Cnu
fmucnd.4 CauFilu
fmucnd.5
Assertion
Ref Expression
fmucnd CauFilu
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem fmucnd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmucnd.1 . . . 4 UnifOn
2 fmucnd.4 . . . 4 CauFilu
3 cfilufbas 21291 . . . 4 UnifOn CauFilu
41, 2, 3syl2anc 665 . . 3
5 fmucnd.2 . . . 4 UnifOn
6 fmucnd.3 . . . 4 Cnu
7 isucn 21280 . . . . 5 UnifOn UnifOn Cnu
87simprbda 627 . . . 4 UnifOn UnifOn Cnu
91, 5, 6, 8syl21anc 1263 . . 3
105elfvexd 5906 . . 3
11 fmucnd.5 . . . 4
1211fbasrn 20886 . . 3
134, 9, 10, 12syl3anc 1264 . 2
14 simplr 760 . . . . . . . 8
15 eqid 2422 . . . . . . . 8
16 imaeq2 5180 . . . . . . . . . 10
1716eqeq2d 2436 . . . . . . . . 9
1817rspcev 3182 . . . . . . . 8
1914, 15, 18sylancl 666 . . . . . . 7
20 imaexg 6741 . . . . . . . . 9 Cnu
21 eqid 2422 . . . . . . . . . 10
2221elrnmpt 5097 . . . . . . . . 9
236, 20, 223syl 18 . . . . . . . 8
2423ad3antrrr 734 . . . . . . 7
2519, 24mpbird 235 . . . . . 6
26 imaeq2 5180 . . . . . . . . 9
2726cbvmptv 4513 . . . . . . . 8
2827rneqi 5077 . . . . . . 7
2911, 28eqtri 2451 . . . . . 6
3025, 29syl6eleqr 2521 . . . . 5
31 ffn 5743 . . . . . . . . 9
329, 31syl 17 . . . . . . . 8
3332ad3antrrr 734 . . . . . . 7
34 simplll 766 . . . . . . . 8
35 fbelss 20835 . . . . . . . . 9
364, 35sylan 473 . . . . . . . 8
3734, 14, 36syl2anc 665 . . . . . . 7
38 fmucndlem 21293 . . . . . . 7
3933, 37, 38syl2anc 665 . . . . . 6
40 eqid 2422 . . . . . . . . 9
4140mpt2fun 6409 . . . . . . . 8
42 funimass2 5672 . . . . . . . 8
4341, 42mpan 674 . . . . . . 7
4443adantl 467 . . . . . 6
4539, 44eqsstr3d 3499 . . . . 5
46 id 23 . . . . . . . 8
4746sqxpeqd 4876 . . . . . . 7
4847sseq1d 3491 . . . . . 6
4948rspcev 3182 . . . . 5
5030, 45, 49syl2anc 665 . . . 4
511adantr 466 . . . . 5 UnifOn
522adantr 466 . . . . 5 CauFilu
535adantr 466 . . . . . 6 UnifOn
546adantr 466 . . . . . 6 Cnu
55 simpr 462 . . . . . 6
56 nfcv 2584 . . . . . . 7
57 nfcv 2584 . . . . . . 7
58 nfcv 2584 . . . . . . 7
59 nfcv 2584 . . . . . . 7
60 simpl 458 . . . . . . . . 9
6160fveq2d 5882 . . . . . . . 8
62 simpr 462 . . . . . . . . 9
6362fveq2d 5882 . . . . . . . 8
6461, 63opeq12d 4192 . . . . . . 7
6556, 57, 58, 59, 64cbvmpt2 6381 . . . . . 6
6651, 53, 54, 55, 65ucnprima 21284 . . . . 5
67 cfiluexsm 21292 . . . . 5 UnifOn CauFilu
6851, 52, 66, 67syl3anc 1264 . . . 4
6950, 68r19.29a 2970 . . 3
7069ralrimiva 2839 . 2
71 iscfilu 21290 . . 3 UnifOn CauFilu
725, 71syl 17 . 2 CauFilu
7313, 70, 72mpbir2and 930 1 CauFilu
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437   wcel 1868  wral 2775  wrex 2776  cvv 3081   wss 3436  cop 4002   class class class wbr 4420   cmpt 4479   cxp 4848  ccnv 4849   crn 4851  cima 4853   wfun 5592   wfn 5593  wf 5594  cfv 5598  (class class class)co 6302   cmpt2 6304  cfbas 18946  UnifOncust 21201   Cnucucn 21277  CauFiluccfilu 21288 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-1st 6804  df-2nd 6805  df-map 7479  df-fbas 18955  df-ust 21202  df-ucn 21278  df-cfilu 21289 This theorem is referenced by:  ucnextcn  21306
 Copyright terms: Public domain W3C validator