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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion cmetcau ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 cmetcau.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 2 3 syl ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5 caun0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝑋 ≠ ∅ )
6 4 5 sylan ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝑋 ≠ ∅ )
7 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑋 )
8 6 7 sylib ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ∃ 𝑥 𝑥 ∈ 𝑋 )
9 simpll ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
10 simpr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
11 simplr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ( Cau ‘ 𝐷 ) )
12 eqid ⊢ ( 𝑦 ∈ ℕ ↦ if ( 𝑦 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑦 ) , 𝑥 ) ) = ( 𝑦 ∈ ℕ ↦ if ( 𝑦 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑦 ) , 𝑥 ) )
13 1 9 10 11 12 cmetcaulem ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
14 8 13 exlimddv ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )