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

Metamath Proof Explorer

Theorem cmetcau

Description: The convergence of a Cauchy sequence in a complete metric space. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 14-Oct-2015)

Ref Expression
Hypothesis cmetcau.1 ⊢ J = MetOpen ⁡ D
Assertion cmetcau ⊢ D ∈ CMet ⁡ X ∧ F ∈ Cau ⁡ D → F ∈ dom ⁡ ⇝t ⁡ J

Proof

Step Hyp Ref Expression
1 cmetcau.1 ⊢ J = MetOpen ⁡ D
2 cmetmet ⊢ D ∈ CMet ⁡ X → D ∈ Met ⁡ X
3 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
4 2 3 syl ⊢ D ∈ CMet ⁡ X → D ∈ ∞Met ⁡ X
5 caun0 ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ Cau ⁡ D → X ≠ ∅
6 4 5 sylan ⊢ D ∈ CMet ⁡ X ∧ F ∈ Cau ⁡ D → X ≠ ∅
7 n0 ⊢ X ≠ ∅ ↔ ∃ x x ∈ X
8 6 7 sylib ⊢ D ∈ CMet ⁡ X ∧ F ∈ Cau ⁡ D → ∃ x x ∈ X
9 simpll ⊢ D ∈ CMet ⁡ X ∧ F ∈ Cau ⁡ D ∧ x ∈ X → D ∈ CMet ⁡ X
10 simpr ⊢ D ∈ CMet ⁡ X ∧ F ∈ Cau ⁡ D ∧ x ∈ X → x ∈ X
11 simplr ⊢ D ∈ CMet ⁡ X ∧ F ∈ Cau ⁡ D ∧ x ∈ X → F ∈ Cau ⁡ D
12 eqid ⊢ y ∈ ℕ ⟼ if y ∈ dom ⁡ F F ⁡ y x = y ∈ ℕ ⟼ if y ∈ dom ⁡ F F ⁡ y x
13 1 9 10 11 12 cmetcaulem ⊢ D ∈ CMet ⁡ X ∧ F ∈ Cau ⁡ D ∧ x ∈ X → F ∈ dom ⁡ ⇝t ⁡ J
14 8 13 exlimddv ⊢ D ∈ CMet ⁡ X ∧ F ∈ Cau ⁡ D → F ∈ dom ⁡ ⇝t ⁡ J