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 𝐹 ) ≠ ∅ )