iscfil3

Description: A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	iscfil3	$⊢ D \in ∞Met (X) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F))$

Proof

Step	Hyp	Ref	Expression
1		cfilfil	$⊢ (D \in ∞Met (X) \land F \in CauFil (D)) \to F \in Fil (X)$
2		cfil3i	$⊢ (D \in ∞Met (X) \land F \in CauFil (D) \land r \in ℝ^{+}) \to \exists x \in X x ball (D) r \in F$
3	2	3expa	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D)) \land r \in ℝ^{+}) \to \exists x \in X x ball (D) r \in F$
4	3	ralrimiva	$⊢ (D \in ∞Met (X) \land F \in CauFil (D)) \to \forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F$
5	1 4	jca	$⊢ (D \in ∞Met (X) \land F \in CauFil (D)) \to (F \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F)$
6		simprl	$⊢ (D \in ∞Met (X) \land (F \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F)) \to F \in Fil (X)$
7		rphalfcl	$⊢ s \in ℝ^{+} \to \frac{s}{2} \in ℝ^{+}$
8	7	adantl	$⊢ ((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \to \frac{s}{2} \in ℝ^{+}$
9		oveq2	$⊢ r = \frac{s}{2} \to x ball (D) r = x ball (D) (\frac{s}{2})$
10	9	eleq1d	$⊢ r = \frac{s}{2} \to (x ball (D) r \in F \leftrightarrow x ball (D) (\frac{s}{2}) \in F)$
11	10	rexbidv	$⊢ r = \frac{s}{2} \to (\exists x \in X x ball (D) r \in F \leftrightarrow \exists x \in X x ball (D) (\frac{s}{2}) \in F)$
12	11	rspcv	$⊢ \frac{s}{2} \in ℝ^{+} \to (\forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F \to \exists x \in X x ball (D) (\frac{s}{2}) \in F)$
13	8 12	syl	$⊢ ((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \to (\forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F \to \exists x \in X x ball (D) (\frac{s}{2}) \in F)$
14		simprr	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \to x ball (D) (\frac{s}{2}) \in F$
15		simp-4l	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to D \in ∞Met (X)$
16		simplrl	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to x \in X$
17		simpllr	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to s \in ℝ^{+}$
18	17	rpred	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to s \in ℝ$
19		simprl	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to u \in (x ball (D) (\frac{s}{2}))$
20		blhalf	$⊢ ((D \in ∞Met (X) \land x \in X) \land (s \in ℝ \land u \in (x ball (D) (\frac{s}{2})))) \to x ball (D) (\frac{s}{2}) \subseteq u ball (D) s$
21	15 16 18 19 20	syl22anc	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to x ball (D) (\frac{s}{2}) \subseteq u ball (D) s$
22		simprr	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to v \in (x ball (D) (\frac{s}{2}))$
23	21 22	sseldd	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to v \in (u ball (D) s)$
24	17	rpxrd	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to s \in ℝ^{*}$
25	17 7	syl	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to \frac{s}{2} \in ℝ^{+}$
26	25	rpxrd	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to \frac{s}{2} \in ℝ^{*}$
27		blssm	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{s}{2} \in ℝ^{*}) \to x ball (D) (\frac{s}{2}) \subseteq X$
28	15 16 26 27	syl3anc	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to x ball (D) (\frac{s}{2}) \subseteq X$
29	28 19	sseldd	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to u \in X$
30	28 22	sseldd	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to v \in X$
31		elbl2	$⊢ ((D \in ∞Met (X) \land s \in ℝ^{*}) \land (u \in X \land v \in X)) \to (v \in (u ball (D) s) \leftrightarrow u D v < s)$
32	15 24 29 30 31	syl22anc	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to (v \in (u ball (D) s) \leftrightarrow u D v < s)$
33	23 32	mpbid	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \land (u \in (x ball (D) (\frac{s}{2})) \land v \in (x ball (D) (\frac{s}{2})))) \to u D v < s$
34	33	ralrimivva	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \to \forall u \in (x ball (D) (\frac{s}{2})) \forall v \in (x ball (D) (\frac{s}{2})) u D v < s$
35		raleq	$⊢ y = x ball (D) (\frac{s}{2}) \to (\forall v \in y u D v < s \leftrightarrow \forall v \in (x ball (D) (\frac{s}{2})) u D v < s)$
36	35	raleqbi1dv	$⊢ y = x ball (D) (\frac{s}{2}) \to (\forall u \in y \forall v \in y u D v < s \leftrightarrow \forall u \in (x ball (D) (\frac{s}{2})) \forall v \in (x ball (D) (\frac{s}{2})) u D v < s)$
37	36	rspcev	$⊢ (x ball (D) (\frac{s}{2}) \in F \land \forall u \in (x ball (D) (\frac{s}{2})) \forall v \in (x ball (D) (\frac{s}{2})) u D v < s) \to \exists y \in F \forall u \in y \forall v \in y u D v < s$
38	14 34 37	syl2anc	$⊢ (((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \land (x \in X \land x ball (D) (\frac{s}{2}) \in F)) \to \exists y \in F \forall u \in y \forall v \in y u D v < s$
39	38	rexlimdvaa	$⊢ ((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \to (\exists x \in X x ball (D) (\frac{s}{2}) \in F \to \exists y \in F \forall u \in y \forall v \in y u D v < s)$
40	13 39	syld	$⊢ ((D \in ∞Met (X) \land F \in Fil (X)) \land s \in ℝ^{+}) \to (\forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F \to \exists y \in F \forall u \in y \forall v \in y u D v < s)$
41	40	ralrimdva	$⊢ (D \in ∞Met (X) \land F \in Fil (X)) \to (\forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F \to \forall s \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u D v < s)$
42	41	impr	$⊢ (D \in ∞Met (X) \land (F \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F)) \to \forall s \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u D v < s$
43		iscfil2	$⊢ D \in ∞Met (X) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall s \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u D v < s))$
44	43	adantr	$⊢ (D \in ∞Met (X) \land (F \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F)) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall s \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u D v < s))$
45	6 42 44	mpbir2and	$⊢ (D \in ∞Met (X) \land (F \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F)) \to F \in CauFil (D)$
46	5 45	impbida	$⊢ D \in ∞Met (X) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall r \in ℝ^{+} \exists x \in X x ball (D) r \in F))$

Metamath Proof Explorer

Theorem iscfil3

Proof