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

Metamath Proof Explorer

Theorem cfilfil

Description: A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015)

		Ref	Expression
	Assertion	cfilfil	$⊢ (D \in ∞Met (X) \land F \in CauFil (D)) \to F \in Fil (X)$

Step	Hyp	Ref	Expression
1		iscfil	$⊢ D \in ∞Met (X) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall x \in ℝ^{+} \exists y \in F D [y \times y] \subseteq [0, x)))$
2	1	simprbda	$⊢ (D \in ∞Met (X) \land F \in CauFil (D)) \to F \in Fil (X)$