fclsfnflim

Description: A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	fclsfnflim	$⊢ F \in Fil (X) \to (A \in (J fClus F) \leftrightarrow \exists g \in Fil (X) (F \subseteq g \land A \in (J fLim g)))$

Proof

Step	Hyp	Ref	Expression
1		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
2	1	adantr	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to F \subseteq 𝒫 X$
3		fclstop	$⊢ A \in (J fClus F) \to J \in Top$
4	3	adantl	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to J \in Top$
5		eqid	$⊢ ⋃ J = ⋃ J$
6	5	neisspw	$⊢ J \in Top \to nei (J) (\{A\}) \subseteq 𝒫 ⋃ J$
7	4 6	syl	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to nei (J) (\{A\}) \subseteq 𝒫 ⋃ J$
8		filunibas	$⊢ F \in Fil (X) \to ⋃ F = X$
9	5	fclsfil	$⊢ A \in (J fClus F) \to F \in Fil (⋃ J)$
10		filunibas	$⊢ F \in Fil (⋃ J) \to ⋃ F = ⋃ J$
11	9 10	syl	$⊢ A \in (J fClus F) \to ⋃ F = ⋃ J$
12	8 11	sylan9req	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to X = ⋃ J$
13	12	pweqd	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to 𝒫 X = 𝒫 ⋃ J$
14	7 13	sseqtrrd	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to nei (J) (\{A\}) \subseteq 𝒫 X$
15	2 14	unssd	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to F \cup nei (J) (\{A\}) \subseteq 𝒫 X$
16		ssun1	$⊢ F \subseteq F \cup nei (J) (\{A\})$
17		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
18		ssn0	$⊢ (F \subseteq F \cup nei (J) (\{A\}) \land F \neq \emptyset) \to F \cup nei (J) (\{A\}) \neq \emptyset$
19	16 17 18	sylancr	$⊢ F \in Fil (X) \to F \cup nei (J) (\{A\}) \neq \emptyset$
20	19	adantr	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to F \cup nei (J) (\{A\}) \neq \emptyset$
21		incom	$⊢ y \cap x = x \cap y$
22		fclsneii	$⊢ (A \in (J fClus F) \land y \in nei (J) (\{A\}) \land x \in F) \to y \cap x \neq \emptyset$
23	21 22	eqnetrrid	$⊢ (A \in (J fClus F) \land y \in nei (J) (\{A\}) \land x \in F) \to x \cap y \neq \emptyset$
24	23	3com23	$⊢ (A \in (J fClus F) \land x \in F \land y \in nei (J) (\{A\})) \to x \cap y \neq \emptyset$
25	24	3expb	$⊢ (A \in (J fClus F) \land (x \in F \land y \in nei (J) (\{A\}))) \to x \cap y \neq \emptyset$
26	25	adantll	$⊢ ((F \in Fil (X) \land A \in (J fClus F)) \land (x \in F \land y \in nei (J) (\{A\}))) \to x \cap y \neq \emptyset$
27	26	ralrimivva	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to \forall x \in F \forall y \in nei (J) (\{A\}) x \cap y \neq \emptyset$
28		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
29	28	adantr	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to F \in fBas (X)$
30		istopon	$⊢ J \in TopOn (X) \leftrightarrow (J \in Top \land X = ⋃ J)$
31	4 12 30	sylanbrc	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to J \in TopOn (X)$
32	5	fclselbas	$⊢ A \in (J fClus F) \to A \in ⋃ J$
33	32	adantl	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to A \in ⋃ J$
34	33 12	eleqtrrd	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to A \in X$
35	34	snssd	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to \{A\} \subseteq X$
36		snnzg	$⊢ A \in (J fClus F) \to \{A\} \neq \emptyset$
37	36	adantl	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to \{A\} \neq \emptyset$
38		neifil	$⊢ (J \in TopOn (X) \land \{A\} \subseteq X \land \{A\} \neq \emptyset) \to nei (J) (\{A\}) \in Fil (X)$
39	31 35 37 38	syl3anc	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to nei (J) (\{A\}) \in Fil (X)$
40		filfbas	$⊢ nei (J) (\{A\}) \in Fil (X) \to nei (J) (\{A\}) \in fBas (X)$
41	39 40	syl	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to nei (J) (\{A\}) \in fBas (X)$
42		fbunfip	$⊢ (F \in fBas (X) \land nei (J) (\{A\}) \in fBas (X)) \to (\neg \emptyset \in fi (F \cup nei (J) (\{A\})) \leftrightarrow \forall x \in F \forall y \in nei (J) (\{A\}) x \cap y \neq \emptyset)$
43	29 41 42	syl2anc	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to (\neg \emptyset \in fi (F \cup nei (J) (\{A\})) \leftrightarrow \forall x \in F \forall y \in nei (J) (\{A\}) x \cap y \neq \emptyset)$
44	27 43	mpbird	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to \neg \emptyset \in fi (F \cup nei (J) (\{A\}))$
45		filtop	$⊢ F \in Fil (X) \to X \in F$
46		fsubbas	$⊢ X \in F \to (fi (F \cup nei (J) (\{A\})) \in fBas (X) \leftrightarrow (F \cup nei (J) (\{A\}) \subseteq 𝒫 X \land F \cup nei (J) (\{A\}) \neq \emptyset \land \neg \emptyset \in fi (F \cup nei (J) (\{A\}))))$
47	45 46	syl	$⊢ F \in Fil (X) \to (fi (F \cup nei (J) (\{A\})) \in fBas (X) \leftrightarrow (F \cup nei (J) (\{A\}) \subseteq 𝒫 X \land F \cup nei (J) (\{A\}) \neq \emptyset \land \neg \emptyset \in fi (F \cup nei (J) (\{A\}))))$
48	47	adantr	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to (fi (F \cup nei (J) (\{A\})) \in fBas (X) \leftrightarrow (F \cup nei (J) (\{A\}) \subseteq 𝒫 X \land F \cup nei (J) (\{A\}) \neq \emptyset \land \neg \emptyset \in fi (F \cup nei (J) (\{A\}))))$
49	15 20 44 48	mpbir3and	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to fi (F \cup nei (J) (\{A\})) \in fBas (X)$
50		fgcl	$⊢ fi (F \cup nei (J) (\{A\})) \in fBas (X) \to X filGen fi (F \cup nei (J) (\{A\})) \in Fil (X)$
51	49 50	syl	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to X filGen fi (F \cup nei (J) (\{A\})) \in Fil (X)$
52		fvex	$⊢ nei (J) (\{A\}) \in V$
53		unexg	$⊢ (F \in Fil (X) \land nei (J) (\{A\}) \in V) \to F \cup nei (J) (\{A\}) \in V$
54	52 53	mpan2	$⊢ F \in Fil (X) \to F \cup nei (J) (\{A\}) \in V$
55		ssfii	$⊢ F \cup nei (J) (\{A\}) \in V \to F \cup nei (J) (\{A\}) \subseteq fi (F \cup nei (J) (\{A\}))$
56	54 55	syl	$⊢ F \in Fil (X) \to F \cup nei (J) (\{A\}) \subseteq fi (F \cup nei (J) (\{A\}))$
57	56	adantr	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to F \cup nei (J) (\{A\}) \subseteq fi (F \cup nei (J) (\{A\}))$
58	57	unssad	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to F \subseteq fi (F \cup nei (J) (\{A\}))$
59		ssfg	$⊢ fi (F \cup nei (J) (\{A\})) \in fBas (X) \to fi (F \cup nei (J) (\{A\})) \subseteq X filGen fi (F \cup nei (J) (\{A\}))$
60	49 59	syl	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to fi (F \cup nei (J) (\{A\})) \subseteq X filGen fi (F \cup nei (J) (\{A\}))$
61	58 60	sstrd	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to F \subseteq X filGen fi (F \cup nei (J) (\{A\}))$
62	57	unssbd	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to nei (J) (\{A\}) \subseteq fi (F \cup nei (J) (\{A\}))$
63	62 60	sstrd	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to nei (J) (\{A\}) \subseteq X filGen fi (F \cup nei (J) (\{A\}))$
64		elflim	$⊢ (J \in TopOn (X) \land X filGen fi (F \cup nei (J) (\{A\})) \in Fil (X)) \to (A \in (J fLim (X filGen fi (F \cup nei (J) (\{A\})))) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq X filGen fi (F \cup nei (J) (\{A\}))))$
65	31 51 64	syl2anc	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to (A \in (J fLim (X filGen fi (F \cup nei (J) (\{A\})))) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq X filGen fi (F \cup nei (J) (\{A\}))))$
66	34 63 65	mpbir2and	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to A \in (J fLim (X filGen fi (F \cup nei (J) (\{A\}))))$
67		sseq2	$⊢ g = X filGen fi (F \cup nei (J) (\{A\})) \to (F \subseteq g \leftrightarrow F \subseteq X filGen fi (F \cup nei (J) (\{A\})))$
68		oveq2	$⊢ g = X filGen fi (F \cup nei (J) (\{A\})) \to J fLim g = J fLim (X filGen fi (F \cup nei (J) (\{A\})))$
69	68	eleq2d	$⊢ g = X filGen fi (F \cup nei (J) (\{A\})) \to (A \in (J fLim g) \leftrightarrow A \in (J fLim (X filGen fi (F \cup nei (J) (\{A\})))))$
70	67 69	anbi12d	$⊢ g = X filGen fi (F \cup nei (J) (\{A\})) \to ((F \subseteq g \land A \in (J fLim g)) \leftrightarrow (F \subseteq X filGen fi (F \cup nei (J) (\{A\})) \land A \in (J fLim (X filGen fi (F \cup nei (J) (\{A\}))))))$
71	70	rspcev	$⊢ (X filGen fi (F \cup nei (J) (\{A\})) \in Fil (X) \land (F \subseteq X filGen fi (F \cup nei (J) (\{A\})) \land A \in (J fLim (X filGen fi (F \cup nei (J) (\{A\})))))) \to \exists g \in Fil (X) (F \subseteq g \land A \in (J fLim g))$
72	51 61 66 71	syl12anc	$⊢ (F \in Fil (X) \land A \in (J fClus F)) \to \exists g \in Fil (X) (F \subseteq g \land A \in (J fLim g))$
73	72	ex	$⊢ F \in Fil (X) \to (A \in (J fClus F) \to \exists g \in Fil (X) (F \subseteq g \land A \in (J fLim g)))$
74		simprl	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to g \in Fil (X)$
75		simprrr	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to A \in (J fLim g)$
76		flimtopon	$⊢ A \in (J fLim g) \to (J \in TopOn (X) \leftrightarrow g \in Fil (X))$
77	75 76	syl	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to (J \in TopOn (X) \leftrightarrow g \in Fil (X))$
78	74 77	mpbird	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to J \in TopOn (X)$
79		simpl	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to F \in Fil (X)$
80		simprrl	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to F \subseteq g$
81		fclsss2	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land F \subseteq g) \to J fClus g \subseteq J fClus F$
82	78 79 80 81	syl3anc	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to J fClus g \subseteq J fClus F$
83		flimfcls	$⊢ J fLim g \subseteq J fClus g$
84	83 75	sseldi	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to A \in (J fClus g)$
85	82 84	sseldd	$⊢ (F \in Fil (X) \land (g \in Fil (X) \land (F \subseteq g \land A \in (J fLim g)))) \to A \in (J fClus F)$
86	85	rexlimdvaa	$⊢ F \in Fil (X) \to (\exists g \in Fil (X) (F \subseteq g \land A \in (J fLim g)) \to A \in (J fClus F))$
87	73 86	impbid	$⊢ F \in Fil (X) \to (A \in (J fClus F) \leftrightarrow \exists g \in Fil (X) (F \subseteq g \land A \in (J fLim g)))$

Metamath Proof Explorer

Theorem fclsfnflim

Proof