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 ⊢ J = MetOpen ⁡ D
Assertion cmetcvg ⊢ D ∈ CMet ⁡ X ∧ F ∈ CauFil ⁡ D → J fLim F ≠ ∅

Proof

Step Hyp Ref Expression
1 iscmet.1 ⊢ J = MetOpen ⁡ D
2 1 iscmet ⊢ D ∈ CMet ⁡ X ↔ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅
3 2 simprbi ⊢ D ∈ CMet ⁡ X → ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅
4 oveq2 ⊢ f = F → J fLim f = J fLim F
5 4 neeq1d ⊢ f = F → J fLim f ≠ ∅ ↔ J fLim F ≠ ∅
6 5 rspccva ⊢ ∀ f ∈ CauFil ⁡ D J fLim f ≠ ∅ ∧ F ∈ CauFil ⁡ D → J fLim F ≠ ∅
7 3 6 sylan ⊢ D ∈ CMet ⁡ X ∧ F ∈ CauFil ⁡ D → J fLim F ≠ ∅