iscfil

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

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

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

Metamath Proof Explorer