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

Theorem equivcfil 22028
 Description: If the metric is "strongly finer" than (meaning that there is a positive real constant such that ), all the -Cauchy filters are also -Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.)
Hypotheses
Ref Expression
equivcau.1
equivcau.2
equivcau.3
equivcau.4
Assertion
Ref Expression
equivcfil CauFil CauFil
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,

Proof of Theorem equivcfil
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 459 . . . . . . . 8
2 equivcau.3 . . . . . . . . 9
32ad2antrr 724 . . . . . . . 8
41, 3rpdivcld 11320 . . . . . . 7
5 oveq2 6285 . . . . . . . . . 10
65eleq1d 2471 . . . . . . . . 9
76rexbidv 2917 . . . . . . . 8
87rspcv 3155 . . . . . . 7
94, 8syl 17 . . . . . 6
10 simpllr 761 . . . . . . . 8
11 eqid 2402 . . . . . . . . . . . 12
12 eqid 2402 . . . . . . . . . . . 12
13 equivcau.1 . . . . . . . . . . . 12
14 equivcau.2 . . . . . . . . . . . 12
15 equivcau.4 . . . . . . . . . . . 12
1611, 12, 13, 14, 2, 15metss2lem 21304 . . . . . . . . . . 11
1716ancom2s 803 . . . . . . . . . 10
1817adantlr 713 . . . . . . . . 9
1918anassrs 646 . . . . . . . 8
2013ad3antrrr 728 . . . . . . . . . 10
21 metxmet 21127 . . . . . . . . . 10
2220, 21syl 17 . . . . . . . . 9
23 simpr 459 . . . . . . . . 9
24 rpxr 11271 . . . . . . . . . 10
2524ad2antlr 725 . . . . . . . . 9
26 blssm 21211 . . . . . . . . 9
2722, 23, 25, 26syl3anc 1230 . . . . . . . 8
28 filss 20644 . . . . . . . . . 10
29283exp2 1215 . . . . . . . . 9
3029com24 87 . . . . . . . 8
3110, 19, 27, 30syl3c 60 . . . . . . 7
3231reximdva 2878 . . . . . 6
339, 32syld 42 . . . . 5
3433ralrimdva 2821 . . . 4
3534imdistanda 691 . . 3
36 metxmet 21127 . . . 4
37 iscfil3 22002 . . . 4 CauFil
3814, 36, 373syl 20 . . 3 CauFil
39 iscfil3 22002 . . . 4 CauFil
4013, 21, 393syl 20 . . 3 CauFil
4135, 38, 403imtr4d 268 . 2 CauFil CauFil
4241ssrdv 3447 1 CauFil CauFil
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   wceq 1405   wcel 1842  wral 2753  wrex 2754   wss 3413   class class class wbr 4394  cfv 5568  (class class class)co 6277   cmul 9526  cxr 9656   cle 9658   cdiv 10246  crp 11264  cxmt 18721  cme 18722  cbl 18723  cmopn 18726  cfil 20636  CauFilccfil 21981 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-cnex 9577  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-mulcom 9585  ax-addass 9586  ax-mulass 9587  ax-distr 9588  ax-i2m1 9589  ax-1ne0 9590  ax-1rid 9591  ax-rnegex 9592  ax-rrecex 9593  ax-cnre 9594  ax-pre-lttri 9595  ax-pre-lttrn 9596  ax-pre-ltadd 9597  ax-pre-mulgt0 9598 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-po 4743  df-so 4744  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-1st 6783  df-2nd 6784  df-er 7347  df-map 7458  df-en 7554  df-dom 7555  df-sdom 7556  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-sub 9842  df-neg 9843  df-div 10247  df-2 10634  df-rp 11265  df-xneg 11370  df-xadd 11371  df-xmul 11372  df-ico 11587  df-psmet 18729  df-xmet 18730  df-met 18731  df-bl 18732  df-fbas 18734  df-fil 20637  df-cfil 21984 This theorem is referenced by:  equivcmet  22044
 Copyright terms: Public domain W3C validator