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 e. ( CMet ` X ) /\ F e. ( CauFil ` D ) ) -> ( J fLim F ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		iscmet.1	|- J = ( MetOpen ` D )
2	1	iscmet	|- ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) ) )
3	2	simprbi	|- ( D e. ( CMet ` X ) -> A. f e. ( 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	|- ( ( A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) /\ F e. ( CauFil ` D ) ) -> ( J fLim F ) =/= (/) )
7	3 6	sylan	|- ( ( D e. ( CMet ` X ) /\ F e. ( CauFil ` D ) ) -> ( J fLim F ) =/= (/) )