This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmetcvg

Description: The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015)

Ref Expression
Hypothesis iscmet.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion cmetcvg ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐽 fLim 𝐹 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 iscmet.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 iscmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
3 2 simprbi ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ )
4 oveq2 ⊢ ( 𝑓 = 𝐹 → ( 𝐽 fLim 𝑓 ) = ( 𝐽 fLim 𝐹 ) )
5 4 neeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝐽 fLim 𝑓 ) ≠ ∅ ↔ ( 𝐽 fLim 𝐹 ) ≠ ∅ ) )
6 5 rspccva ⊢ ( ( ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐽 fLim 𝐹 ) ≠ ∅ )
7 3 6 sylan ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐽 fLim 𝐹 ) ≠ ∅ )