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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion flimcfil ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝐹 ∈ ( CauFil ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 lmcau.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
3 2 flimfil ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
4 3 adantl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
5 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
6 5 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑋 = ∪ 𝐽 )
7 6 fveq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) → ( Fil ‘ 𝑋 ) = ( Fil ‘ ∪ 𝐽 ) )
8 4 7 eleqtrrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
9 2 flimelbas ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐴 ∈ ∪ 𝐽 )
10 9 ad2antlr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ∪ 𝐽 )
11 5 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑋 = ∪ 𝐽 )
12 10 11 eleqtrrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ 𝑋 )
13 simplr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) )
14 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
15 14 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐽 ∈ Top )
16 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17 rpxr ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ* )
18 17 adantl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ* )
19 1 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ ℝ* ) → ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐽 )
20 16 12 18 19 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐽 )
21 simpr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
22 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) )
23 16 12 21 22 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) )
24 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐽 ∧ 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ) → ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
25 15 20 23 24 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
26 flimnei ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 )
27 13 25 26 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 )
28 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) = ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) )
29 28 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 ↔ ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 ) )
30 29 rspcev ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 )
31 12 27 30 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 )
32 31 ralrimiva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑋 ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 )
33 iscfil3 ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑋 ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 ) ) )
34 33 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑋 ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐹 ) ) )
35 8 32 34 mpbir2and ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝐹 ∈ ( CauFil ‘ 𝐷 ) )