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 ( ⇝𝑡 ‘ 𝐽 ) )