iscfil2

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

		Ref	Expression
	Assertion	iscfil2	$⊢ D \in ∞Met (X) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall x \in ℝ^{+} \exists y \in F \forall z \in y \forall w \in y z D w < x))$

Proof

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		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
3	2	ad3antrrr	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to D : X \times X ⟶ ℝ^{*}$
4	3	ffund	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to Fun D$
5		filelss	$⊢ (F \in Fil (X) \land y \in F) \to y \subseteq X$
6	5	ad4ant24	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to y \subseteq X$
7		xpss12	$⊢ (y \subseteq X \land y \subseteq X) \to y \times y \subseteq X \times X$
8	6 6 7	syl2anc	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to y \times y \subseteq X \times X$
9	3	fdmd	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to dom D = X \times X$
10	8 9	sseqtrrd	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to y \times y \subseteq dom D$
11		funimassov	$⊢ (Fun D \land y \times y \subseteq dom D) \to (D [y \times y] \subseteq [0, x) \leftrightarrow \forall z \in y \forall w \in y z D w \in [0, x))$
12	4 10 11	syl2anc	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to (D [y \times y] \subseteq [0, x) \leftrightarrow \forall z \in y \forall w \in y z D w \in [0, x))$
13		0xr	$⊢ 0 \in ℝ^{*}$
14	13	a1i	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to 0 \in ℝ^{*}$
15		simpllr	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to x \in ℝ^{+}$
16	15	rpxrd	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to x \in ℝ^{*}$
17		simp-4l	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to D \in ∞Met (X)$
18	6	sselda	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land z \in y) \to z \in X$
19	18	adantrr	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to z \in X$
20	6	sselda	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land w \in y) \to w \in X$
21	20	adantrl	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to w \in X$
22		xmetcl	$⊢ (D \in ∞Met (X) \land z \in X \land w \in X) \to z D w \in ℝ^{*}$
23	17 19 21 22	syl3anc	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to z D w \in ℝ^{*}$
24		xmetge0	$⊢ (D \in ∞Met (X) \land z \in X \land w \in X) \to 0 \leq z D w$
25	17 19 21 24	syl3anc	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to 0 \leq z D w$
26		elico1	$⊢ (0 \in ℝ^{} \land x \in ℝ^{}) \to (z D w \in [0, x) \leftrightarrow (z D w \in ℝ^{*} \land 0 \leq z D w \land z D w < x))$
27		df-3an	$⊢ (z D w \in ℝ^{} \land 0 \leq z D w \land z D w < x) \leftrightarrow ((z D w \in ℝ^{} \land 0 \leq z D w) \land z D w < x)$
28	26 27	bitrdi	$⊢ (0 \in ℝ^{} \land x \in ℝ^{}) \to (z D w \in [0, x) \leftrightarrow ((z D w \in ℝ^{*} \land 0 \leq z D w) \land z D w < x))$
29	28	baibd	$⊢ ((0 \in ℝ^{} \land x \in ℝ^{}) \land (z D w \in ℝ^{*} \land 0 \leq z D w)) \to (z D w \in [0, x) \leftrightarrow z D w < x)$
30	14 16 23 25 29	syl22anc	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \land (z \in y \land w \in y)) \to (z D w \in [0, x) \leftrightarrow z D w < x)$
31	30	2ralbidva	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to (\forall z \in y \forall w \in y z D w \in [0, x) \leftrightarrow \forall z \in y \forall w \in y z D w < x)$
32	12 31	bitrd	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \land y \in F) \to (D [y \times y] \subseteq [0, x) \leftrightarrow \forall z \in y \forall w \in y z D w < x)$
33	32	rexbidva	$⊢ ((D \in ∞Met (X) \land F \in Fil (X)) \land x \in ℝ^{+}) \to (\exists y \in F D [y \times y] \subseteq [0, x) \leftrightarrow \exists y \in F \forall z \in y \forall w \in y z D w < x)$
34	33	ralbidva	$⊢ (D \in ∞Met (X) \land F \in Fil (X)) \to (\forall x \in ℝ^{+} \exists y \in F D [y \times y] \subseteq [0, x) \leftrightarrow \forall x \in ℝ^{+} \exists y \in F \forall z \in y \forall w \in y z D w < x)$
35	34	pm5.32da	$⊢ D \in ∞Met (X) \to ((F \in Fil (X) \land \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 \forall z \in y \forall w \in y z D w < x))$
36	1 35	bitrd	$⊢ D \in ∞Met (X) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall x \in ℝ^{+} \exists y \in F \forall z \in y \forall w \in y z D w < x))$

Metamath Proof Explorer

Theorem iscfil2

Proof