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

Metamath Proof Explorer

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 ) =/= (/) )