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

Theorem flimcfil 22281
 Description: Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
Hypothesis
Ref Expression
lmcau.1
Assertion
Ref Expression
flimcfil CauFil

Proof of Theorem flimcfil
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2422 . . . . 5
21flimfil 20982 . . . 4
4 lmcau.1 . . . . . 6
54mopnuni 21454 . . . . 5
65adantr 466 . . . 4
76fveq2d 5885 . . 3
83, 7eleqtrrd 2510 . 2
91flimelbas 20981 . . . . . 6
109ad2antlr 731 . . . . 5
115ad2antrr 730 . . . . 5
1210, 11eleqtrrd 2510 . . . 4
13 simplr 760 . . . . 5
144mopntop 21453 . . . . . . 7
1514ad2antrr 730 . . . . . 6
16 simpll 758 . . . . . . 7
17 rpxr 11316 . . . . . . . 8
1817adantl 467 . . . . . . 7
194blopn 21513 . . . . . . 7
2016, 12, 18, 19syl3anc 1264 . . . . . 6
21 simpr 462 . . . . . . 7
22 blcntr 21426 . . . . . . 7
2316, 12, 21, 22syl3anc 1264 . . . . . 6
24 opnneip 20133 . . . . . 6
2515, 20, 23, 24syl3anc 1264 . . . . 5
26 flimnei 20980 . . . . 5
2713, 25, 26syl2anc 665 . . . 4
28 oveq1 6312 . . . . . 6
2928eleq1d 2491 . . . . 5
3029rspcev 3182 . . . 4
3112, 27, 30syl2anc 665 . . 3
3231ralrimiva 2836 . 2
33 iscfil3 22241 . . 3 CauFil