Theorem iscfil

Description: The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		cfilfval	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{CauFil}\left(D\right)=\left\{f\in \mathrm{Fil}\left(X\right)|\forall x\in {ℝ}^{+}\exists y\in fD\left[y\times y\right]\subseteq \left[0,x\right)\right\}$$
2	1	eleq2d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(F\in \mathrm{CauFil}\left(D\right)\leftrightarrow F\in \left\{f\in \mathrm{Fil}\left(X\right)|\forall x\in {ℝ}^{+}\exists y\in fD\left[y\times y\right]\subseteq \left[0,x\right)\right\}\right)$$
3		rexeq	$$⊢f=F\to \left(\exists y\in fD\left[y\times y\right]\subseteq \left[0,x\right)\leftrightarrow \exists y\in FD\left[y\times y\right]\subseteq \left[0,x\right)\right)$$
4	3	ralbidv	$$⊢f=F\to \left(\forall x\in {ℝ}^{+}\exists y\in fD\left[y\times y\right]\subseteq \left[0,x\right)\leftrightarrow \forall x\in {ℝ}^{+}\exists y\in FD\left[y\times y\right]\subseteq \left[0,x\right)\right)$$
5	4	elrab	$$⊢F\in \left\{f\in \mathrm{Fil}\left(X\right)|\forall x\in {ℝ}^{+}\exists y\in fD\left[y\times y\right]\subseteq \left[0,x\right)\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)$$
6	2 5	syl6bb	$$⊢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)$$