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 \in CMet (X) \land F \in CauFil (D)) \to J fLim F \neq \emptyset$

Step	Hyp	Ref	Expression
1		iscmet.1	$⊢ J = MetOpen (D)$
2	1	iscmet	$⊢ D \in CMet (X) \leftrightarrow (D \in Met (X) \land \forall f \in CauFil (D) J fLim f \neq \emptyset)$
3	2	simprbi	$⊢ D \in CMet (X) \to \forall f \in CauFil (D) J fLim f \neq \emptyset$
4		oveq2	$⊢ f = F \to J fLim f = J fLim F$
5	4	neeq1d	$⊢ f = F \to (J fLim f \neq \emptyset \leftrightarrow J fLim F \neq \emptyset)$
6	5	rspccva	$⊢ (\forall f \in CauFil (D) J fLim f \neq \emptyset \land F \in CauFil (D)) \to J fLim F \neq \emptyset$
7	3 6	sylan	$⊢ (D \in CMet (X) \land F \in CauFil (D)) \to J fLim F \neq \emptyset$

Metamath Proof Explorer