Metamath Proof Explorer

Theorem flimcfil

Description: Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis lmcau.1 
|- J = ( MetOpen ` D )
Assertion flimcfil 
|- ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> F e. ( CauFil ` D ) )

Proof

Step Hyp Ref Expression
1 lmcau.1 
 |-  J = ( MetOpen ` D )
2 eqid 
 |-  U. J = U. J
3 2 flimfil 
 |-  ( A e. ( J fLim F ) -> F e. ( Fil ` U. J ) )
4 3 adantl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> F e. ( Fil ` U. J ) )
5 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
6 5 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> X = U. J )
7 6 fveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> ( Fil ` X ) = ( Fil ` U. J ) )
8 4 7 eleqtrrd 
 |-  ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> F e. ( Fil ` X ) )
9 2 flimelbas 
 |-  ( A e. ( J fLim F ) -> A e. U. J )
10 9 ad2antlr 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> A e. U. J )
11 5 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> X = U. J )
12 10 11 eleqtrrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> A e. X )
13 simplr 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> A e. ( J fLim F ) )
14 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
15 14 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> J e. Top )
16 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> D e. ( *Met ` X ) )
17 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
18 17 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> x e. RR* )
19 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ x e. RR* ) -> ( A ( ball ` D ) x ) e. J )
20 16 12 18 19 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> ( A ( ball ` D ) x ) e. J )
21 simpr 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> x e. RR+ )
22 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ x e. RR+ ) -> A e. ( A ( ball ` D ) x ) )
23 16 12 21 22 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> A e. ( A ( ball ` D ) x ) )
24 opnneip 
 |-  ( ( J e. Top /\ ( A ( ball ` D ) x ) e. J /\ A e. ( A ( ball ` D ) x ) ) -> ( A ( ball ` D ) x ) e. ( ( nei ` J ) ` { A } ) )
25 15 20 23 24 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> ( A ( ball ` D ) x ) e. ( ( nei ` J ) ` { A } ) )
26 flimnei 
 |-  ( ( A e. ( J fLim F ) /\ ( A ( ball ` D ) x ) e. ( ( nei ` J ) ` { A } ) ) -> ( A ( ball ` D ) x ) e. F )
27 13 25 26 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> ( A ( ball ` D ) x ) e. F )
28 oveq1 
 |-  ( y = A -> ( y ( ball ` D ) x ) = ( A ( ball ` D ) x ) )
29 28 eleq1d 
 |-  ( y = A -> ( ( y ( ball ` D ) x ) e. F <-> ( A ( ball ` D ) x ) e. F ) )
30 29 rspcev 
 |-  ( ( A e. X /\ ( A ( ball ` D ) x ) e. F ) -> E. y e. X ( y ( ball ` D ) x ) e. F )
31 12 27 30 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) /\ x e. RR+ ) -> E. y e. X ( y ( ball ` D ) x ) e. F )
32 31 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> A. x e. RR+ E. y e. X ( y ( ball ` D ) x ) e. F )
33 iscfil3 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. X ( y ( ball ` D ) x ) e. F ) ) )
34 33 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. X ( y ( ball ` D ) x ) e. F ) ) )
35 8 32 34 mpbir2and 
 |-  ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> F e. ( CauFil ` D ) )