Metamath Proof Explorer

Theorem cfili

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

		Ref	Expression
	Assertion	cfili	$⊢ (F \in CauFil (D) \land R \in ℝ^{+}) \to \exists x \in F \forall y \in x \forall z \in x y D z < R$

Proof

Step	Hyp	Ref	Expression
1		df-cfil	$⊢ CauFil = (d \in ⋃ ran ∞Met ⟼ \{f \in Fil (dom dom d) \| \forall x \in ℝ^{+} \exists y \in f d [y \times y] \subseteq [0, x)\})$
2	1	mptrcl	$⊢ F \in CauFil (D) \to D \in ⋃ ran ∞Met$
3		xmetunirn	$⊢ D \in ⋃ ran ∞Met \leftrightarrow D \in ∞Met (dom dom D)$
4	2 3	sylib	$⊢ F \in CauFil (D) \to D \in ∞Met (dom dom D)$
5		iscfil2	$⊢ D \in ∞Met (dom dom D) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (dom dom D) \land \forall r \in ℝ^{+} \exists x \in F \forall y \in x \forall z \in x y D z < r))$
6	4 5	syl	$⊢ F \in CauFil (D) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (dom dom D) \land \forall r \in ℝ^{+} \exists x \in F \forall y \in x \forall z \in x y D z < r))$
7	6	ibi	$⊢ F \in CauFil (D) \to (F \in Fil (dom dom D) \land \forall r \in ℝ^{+} \exists x \in F \forall y \in x \forall z \in x y D z < r)$
8	7	simprd	$⊢ F \in CauFil (D) \to \forall r \in ℝ^{+} \exists x \in F \forall y \in x \forall z \in x y D z < r$
9		breq2	$⊢ r = R \to (y D z < r \leftrightarrow y D z < R)$
10	9	2ralbidv	$⊢ r = R \to (\forall y \in x \forall z \in x y D z < r \leftrightarrow \forall y \in x \forall z \in x y D z < R)$
11	10	rexbidv	$⊢ r = R \to (\exists x \in F \forall y \in x \forall z \in x y D z < r \leftrightarrow \exists x \in F \forall y \in x \forall z \in x y D z < R)$
12	11	rspccva	$⊢ (\forall r \in ℝ^{+} \exists x \in F \forall y \in x \forall z \in x y D z < r \land R \in ℝ^{+}) \to \exists x \in F \forall y \in x \forall z \in x y D z < R$
13	8 12	sylan	$⊢ (F \in CauFil (D) \land R \in ℝ^{+}) \to \exists x \in F \forall y \in x \forall z \in x y D z < R$