cfilfcls

Description: Similar to ultrafilters ( uffclsflim ), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	cfilfcls.1	$⊢ J = MetOpen (D)$
	cfilfcls.2	$⊢ X = dom dom D$
Assertion	cfilfcls	$⊢ F \in CauFil (D) \to J fClus F = J fLim F$

Proof

Step	Hyp	Ref	Expression
1		cfilfcls.1	$⊢ J = MetOpen (D)$
2		cfilfcls.2	$⊢ X = dom dom D$
3		eqid	$⊢ ⋃ J = ⋃ J$
4	3	fclselbas	$⊢ x \in (J fClus F) \to x \in ⋃ J$
5	4	adantl	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to x \in ⋃ J$
6		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)\})$
7	6	mptrcl	$⊢ F \in CauFil (D) \to D \in ⋃ ran ∞Met$
8		xmetunirn	$⊢ D \in ⋃ ran ∞Met \leftrightarrow D \in ∞Met (dom dom D)$
9	7 8	sylib	$⊢ F \in CauFil (D) \to D \in ∞Met (dom dom D)$
10	2	fveq2i	$⊢ ∞Met (X) = ∞Met (dom dom D)$
11	9 10	eleqtrrdi	$⊢ F \in CauFil (D) \to D \in ∞Met (X)$
12	11	adantr	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to D \in ∞Met (X)$
13	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
14	12 13	syl	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to J \in TopOn (X)$
15		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
16	14 15	syl	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to X = ⋃ J$
17	5 16	eleqtrrd	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to x \in X$
18	1	mopni2	$⊢ (D \in ∞Met (X) \land y \in J \land x \in y) \to \exists r \in ℝ^{+} x ball (D) r \subseteq y$
19	18	3expb	$⊢ (D \in ∞Met (X) \land (y \in J \land x \in y)) \to \exists r \in ℝ^{+} x ball (D) r \subseteq y$
20	12 19	sylan	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land (y \in J \land x \in y)) \to \exists r \in ℝ^{+} x ball (D) r \subseteq y$
21		cfilfil	$⊢ (D \in ∞Met (X) \land F \in CauFil (D)) \to F \in Fil (X)$
22	11 21	mpancom	$⊢ F \in CauFil (D) \to F \in Fil (X)$
23	22	adantr	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to F \in Fil (X)$
24	23	ad2antrr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land (y \in J \land x \in y)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to F \in Fil (X)$
25	12	adantr	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \to D \in ∞Met (X)$
26		simpll	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \to F \in CauFil (D)$
27		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
28	27	adantl	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{+}$
29		rphalfcl	$⊢ \frac{r}{2} \in ℝ^{+} \to \frac{\frac{r}{2}}{2} \in ℝ^{+}$
30	28 29	syl	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \to \frac{\frac{r}{2}}{2} \in ℝ^{+}$
31		cfil3i	$⊢ (D \in ∞Met (X) \land F \in CauFil (D) \land \frac{\frac{r}{2}}{2} \in ℝ^{+}) \to \exists y \in X y ball (D) (\frac{\frac{r}{2}}{2}) \in F$
32	25 26 30 31	syl3anc	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \to \exists y \in X y ball (D) (\frac{\frac{r}{2}}{2}) \in F$
33	23	ad2antrr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to F \in Fil (X)$
34		simprr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to y ball (D) (\frac{\frac{r}{2}}{2}) \in F$
35	25	adantr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to D \in ∞Met (X)$
36	17	ad2antrr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to x \in X$
37		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
38	37	ad2antlr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to r \in ℝ^{*}$
39		blssm	$⊢ (D \in ∞Met (X) \land x \in X \land r \in ℝ^{*}) \to x ball (D) r \subseteq X$
40	35 36 38 39	syl3anc	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to x ball (D) r \subseteq X$
41		simpllr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to x \in (J fClus F)$
42	28	adantr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to \frac{r}{2} \in ℝ^{+}$
43	42	rpxrd	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to \frac{r}{2} \in ℝ^{*}$
44	1	blopn	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{r}{2} \in ℝ^{*}) \to x ball (D) (\frac{r}{2}) \in J$
45	35 36 43 44	syl3anc	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to x ball (D) (\frac{r}{2}) \in J$
46		blcntr	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{r}{2} \in ℝ^{+}) \to x \in (x ball (D) (\frac{r}{2}))$
47	35 36 42 46	syl3anc	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to x \in (x ball (D) (\frac{r}{2}))$
48		fclsopni	$⊢ (x \in (J fClus F) \land (x ball (D) (\frac{r}{2}) \in J \land x \in (x ball (D) (\frac{r}{2})) \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to (x ball (D) (\frac{r}{2})) \cap (y ball (D) (\frac{\frac{r}{2}}{2})) \neq \emptyset$
49	41 45 47 34 48	syl13anc	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to (x ball (D) (\frac{r}{2})) \cap (y ball (D) (\frac{\frac{r}{2}}{2})) \neq \emptyset$
50		n0	$⊢ (x ball (D) (\frac{r}{2})) \cap (y ball (D) (\frac{\frac{r}{2}}{2})) \neq \emptyset \leftrightarrow \exists z z \in ((x ball (D) (\frac{r}{2})) \cap (y ball (D) (\frac{\frac{r}{2}}{2})))$
51	49 50	sylib	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to \exists z z \in ((x ball (D) (\frac{r}{2})) \cap (y ball (D) (\frac{\frac{r}{2}}{2})))$
52		elin	$⊢ z \in ((x ball (D) (\frac{r}{2})) \cap (y ball (D) (\frac{\frac{r}{2}}{2}))) \leftrightarrow (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))$
53	35	adantr	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to D \in ∞Met (X)$
54		simplrl	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to y \in X$
55	42	adantr	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to \frac{r}{2} \in ℝ^{+}$
56	55	rpred	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to \frac{r}{2} \in ℝ$
57		simprr	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to z \in (y ball (D) (\frac{\frac{r}{2}}{2}))$
58		blhalf	$⊢ ((D \in ∞Met (X) \land y \in X) \land (\frac{r}{2} \in ℝ \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to y ball (D) (\frac{\frac{r}{2}}{2}) \subseteq z ball (D) (\frac{r}{2})$
59	53 54 56 57 58	syl22anc	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to y ball (D) (\frac{\frac{r}{2}}{2}) \subseteq z ball (D) (\frac{r}{2})$
60		blssm	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{r}{2} \in ℝ^{*}) \to x ball (D) (\frac{r}{2}) \subseteq X$
61	35 36 43 60	syl3anc	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to x ball (D) (\frac{r}{2}) \subseteq X$
62	61	sselda	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land z \in (x ball (D) (\frac{r}{2}))) \to z \in X$
63	62	adantrr	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to z \in X$
64		simpllr	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to r \in ℝ^{+}$
65	64	rpred	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to r \in ℝ$
66		simprl	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to z \in (x ball (D) (\frac{r}{2}))$
67	55	rpxrd	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to \frac{r}{2} \in ℝ^{*}$
68	36	adantr	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to x \in X$
69		blcom	$⊢ ((D \in ∞Met (X) \land \frac{r}{2} \in ℝ^{*}) \land (x \in X \land z \in X)) \to (z \in (x ball (D) (\frac{r}{2})) \leftrightarrow x \in (z ball (D) (\frac{r}{2})))$
70	53 67 68 63 69	syl22anc	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to (z \in (x ball (D) (\frac{r}{2})) \leftrightarrow x \in (z ball (D) (\frac{r}{2})))$
71	66 70	mpbid	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to x \in (z ball (D) (\frac{r}{2}))$
72		blhalf	$⊢ ((D \in ∞Met (X) \land z \in X) \land (r \in ℝ \land x \in (z ball (D) (\frac{r}{2})))) \to z ball (D) (\frac{r}{2}) \subseteq x ball (D) r$
73	53 63 65 71 72	syl22anc	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to z ball (D) (\frac{r}{2}) \subseteq x ball (D) r$
74	59 73	sstrd	$⊢ ((((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \land (z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2})))) \to y ball (D) (\frac{\frac{r}{2}}{2}) \subseteq x ball (D) r$
75	74	ex	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to ((z \in (x ball (D) (\frac{r}{2})) \land z \in (y ball (D) (\frac{\frac{r}{2}}{2}))) \to y ball (D) (\frac{\frac{r}{2}}{2}) \subseteq x ball (D) r)$
76	52 75	biimtrid	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to (z \in ((x ball (D) (\frac{r}{2})) \cap (y ball (D) (\frac{\frac{r}{2}}{2}))) \to y ball (D) (\frac{\frac{r}{2}}{2}) \subseteq x ball (D) r)$
77	76	exlimdv	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to (\exists z z \in ((x ball (D) (\frac{r}{2})) \cap (y ball (D) (\frac{\frac{r}{2}}{2}))) \to y ball (D) (\frac{\frac{r}{2}}{2}) \subseteq x ball (D) r)$
78	51 77	mpd	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to y ball (D) (\frac{\frac{r}{2}}{2}) \subseteq x ball (D) r$
79		filss	$⊢ (F \in Fil (X) \land (y ball (D) (\frac{\frac{r}{2}}{2}) \in F \land x ball (D) r \subseteq X \land y ball (D) (\frac{\frac{r}{2}}{2}) \subseteq x ball (D) r)) \to x ball (D) r \in F$
80	33 34 40 78 79	syl13anc	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \land (y \in X \land y ball (D) (\frac{\frac{r}{2}}{2}) \in F)) \to x ball (D) r \in F$
81	32 80	rexlimddv	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land r \in ℝ^{+}) \to x ball (D) r \in F$
82	81	ad2ant2r	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land (y \in J \land x \in y)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to x ball (D) r \in F$
83		toponss	$⊢ (J \in TopOn (X) \land y \in J) \to y \subseteq X$
84	83	adantrr	$⊢ (J \in TopOn (X) \land (y \in J \land x \in y)) \to y \subseteq X$
85	14 84	sylan	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land (y \in J \land x \in y)) \to y \subseteq X$
86	85	adantr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land (y \in J \land x \in y)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to y \subseteq X$
87		simprr	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land (y \in J \land x \in y)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to x ball (D) r \subseteq y$
88		filss	$⊢ (F \in Fil (X) \land (x ball (D) r \in F \land y \subseteq X \land x ball (D) r \subseteq y)) \to y \in F$
89	24 82 86 87 88	syl13anc	$⊢ (((F \in CauFil (D) \land x \in (J fClus F)) \land (y \in J \land x \in y)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to y \in F$
90	20 89	rexlimddv	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land (y \in J \land x \in y)) \to y \in F$
91	90	expr	$⊢ ((F \in CauFil (D) \land x \in (J fClus F)) \land y \in J) \to (x \in y \to y \in F)$
92	91	ralrimiva	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to \forall y \in J (x \in y \to y \in F)$
93		flimopn	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (x \in (J fLim F) \leftrightarrow (x \in X \land \forall y \in J (x \in y \to y \in F)))$
94	14 23 93	syl2anc	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to (x \in (J fLim F) \leftrightarrow (x \in X \land \forall y \in J (x \in y \to y \in F)))$
95	17 92 94	mpbir2and	$⊢ (F \in CauFil (D) \land x \in (J fClus F)) \to x \in (J fLim F)$
96	95	ex	$⊢ F \in CauFil (D) \to (x \in (J fClus F) \to x \in (J fLim F))$
97	96	ssrdv	$⊢ F \in CauFil (D) \to J fClus F \subseteq J fLim F$
98		flimfcls	$⊢ J fLim F \subseteq J fClus F$
99	98	a1i	$⊢ F \in CauFil (D) \to J fLim F \subseteq J fClus F$
100	97 99	eqssd	$⊢ F \in CauFil (D) \to J fClus F = J fLim F$

Metamath Proof Explorer

Theorem cfilfcls

Proof