Theorem cfilfil

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

	Ref	Expression
Assertion	cfilfil	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge F\in \mathrm{CauFil}\left(D\right)\right)\to F\in \mathrm{Fil}\left(X\right)$$

Proof

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