flimfnfcls

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim , this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

		Ref	Expression
	Hypothesis	flimfnfcls.x	$⊢ X = ⋃ J$
	Assertion	flimfnfcls	$⊢ F \in Fil (X) \to (A \in (J fLim F) \leftrightarrow \forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)))$

Proof

Step	Hyp	Ref	Expression
1		flimfnfcls.x	$⊢ X = ⋃ J$
2		flimfcls	$⊢ J fLim g \subseteq J fClus g$
3		flimtop	$⊢ A \in (J fLim F) \to J \in Top$
4	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
5	3 4	sylib	$⊢ A \in (J fLim F) \to J \in TopOn (X)$
6	5	ad2antrr	$⊢ ((A \in (J fLim F) \land g \in Fil (X)) \land F \subseteq g) \to J \in TopOn (X)$
7		simplr	$⊢ ((A \in (J fLim F) \land g \in Fil (X)) \land F \subseteq g) \to g \in Fil (X)$
8		simpr	$⊢ ((A \in (J fLim F) \land g \in Fil (X)) \land F \subseteq g) \to F \subseteq g$
9		flimss2	$⊢ (J \in TopOn (X) \land g \in Fil (X) \land F \subseteq g) \to J fLim F \subseteq J fLim g$
10	6 7 8 9	syl3anc	$⊢ ((A \in (J fLim F) \land g \in Fil (X)) \land F \subseteq g) \to J fLim F \subseteq J fLim g$
11		simpll	$⊢ ((A \in (J fLim F) \land g \in Fil (X)) \land F \subseteq g) \to A \in (J fLim F)$
12	10 11	sseldd	$⊢ ((A \in (J fLim F) \land g \in Fil (X)) \land F \subseteq g) \to A \in (J fLim g)$
13	2 12	sselid	$⊢ ((A \in (J fLim F) \land g \in Fil (X)) \land F \subseteq g) \to A \in (J fClus g)$
14	13	ex	$⊢ (A \in (J fLim F) \land g \in Fil (X)) \to (F \subseteq g \to A \in (J fClus g))$
15	14	ralrimiva	$⊢ A \in (J fLim F) \to \forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g))$
16		sseq2	$⊢ g = F \to (F \subseteq g \leftrightarrow F \subseteq F)$
17		oveq2	$⊢ g = F \to J fClus g = J fClus F$
18	17	eleq2d	$⊢ g = F \to (A \in (J fClus g) \leftrightarrow A \in (J fClus F))$
19	16 18	imbi12d	$⊢ g = F \to ((F \subseteq g \to A \in (J fClus g)) \leftrightarrow (F \subseteq F \to A \in (J fClus F)))$
20	19	rspcv	$⊢ F \in Fil (X) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to (F \subseteq F \to A \in (J fClus F)))$
21		ssid	$⊢ F \subseteq F$
22		id	$⊢ (F \subseteq F \to A \in (J fClus F)) \to (F \subseteq F \to A \in (J fClus F))$
23	21 22	mpi	$⊢ (F \subseteq F \to A \in (J fClus F)) \to A \in (J fClus F)$
24		fclstop	$⊢ A \in (J fClus F) \to J \in Top$
25	1	fclselbas	$⊢ A \in (J fClus F) \to A \in X$
26	24 25	jca	$⊢ A \in (J fClus F) \to (J \in Top \land A \in X)$
27	23 26	syl	$⊢ (F \subseteq F \to A \in (J fClus F)) \to (J \in Top \land A \in X)$
28	20 27	syl6	$⊢ F \in Fil (X) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to (J \in Top \land A \in X))$
29		disjdif	$⊢ o \cap (X ∖ o) = \emptyset$
30		simpll	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to F \in Fil (X)$
31		simplrl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to J \in Top$
32	1	topopn	$⊢ J \in Top \to X \in J$
33	31 32	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X \in J$
34		pwexg	$⊢ X \in J \to 𝒫 X \in V$
35		rabexg	$⊢ 𝒫 X \in V \to \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in V$
36	33 34 35	3syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in V$
37		unexg	$⊢ (F \in Fil (X) \land \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in V) \to F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in V$
38	30 36 37	syl2anc	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in V$
39		ssfii	$⊢ F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in V \to F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})$
40	38 39	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})$
41		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
42		ssrab2	$⊢ \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq 𝒫 X$
43	42	a1i	$⊢ F \in Fil (X) \to \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq 𝒫 X$
44	41 43	unssd	$⊢ F \in Fil (X) \to F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq 𝒫 X$
45	44	ad2antrr	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq 𝒫 X$
46		ssun2	$⊢ \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}$
47		sseq2	$⊢ x = X ∖ o \to (X ∖ o \subseteq x \leftrightarrow X ∖ o \subseteq X ∖ o)$
48		difss	$⊢ X ∖ o \subseteq X$
49		elpw2g	$⊢ X \in J \to (X ∖ o \in 𝒫 X \leftrightarrow X ∖ o \subseteq X)$
50	33 49	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (X ∖ o \in 𝒫 X \leftrightarrow X ∖ o \subseteq X)$
51	48 50	mpbiri	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X ∖ o \in 𝒫 X$
52		ssid	$⊢ X ∖ o \subseteq X ∖ o$
53	52	a1i	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X ∖ o \subseteq X ∖ o$
54	47 51 53	elrabd	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X ∖ o \in \{x \in 𝒫 X \| X ∖ o \subseteq x\}$
55	46 54	sselid	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X ∖ o \in (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})$
56	55	ne0d	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \neq \emptyset$
57		sseq2	$⊢ x = z \to (X ∖ o \subseteq x \leftrightarrow X ∖ o \subseteq z)$
58	57	elrab	$⊢ z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\} \leftrightarrow (z \in 𝒫 X \land X ∖ o \subseteq z)$
59	58	simprbi	$⊢ z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\} \to X ∖ o \subseteq z$
60	59	ad2antll	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to X ∖ o \subseteq z$
61		sslin	$⊢ X ∖ o \subseteq z \to y \cap (X ∖ o) \subseteq y \cap z$
62	60 61	syl	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to y \cap (X ∖ o) \subseteq y \cap z$
63		simprrr	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to \neg o \in F$
64	63	adantr	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to \neg o \in F$
65		inssdif0	$⊢ y \cap X \subseteq o \leftrightarrow y \cap (X ∖ o) = \emptyset$
66		simplll	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to F \in Fil (X)$
67		simprl	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to y \in F$
68		filelss	$⊢ (F \in Fil (X) \land y \in F) \to y \subseteq X$
69	66 67 68	syl2anc	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to y \subseteq X$
70		df-ss	$⊢ y \subseteq X \leftrightarrow y \cap X = y$
71	69 70	sylib	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to y \cap X = y$
72	71	sseq1d	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to (y \cap X \subseteq o \leftrightarrow y \subseteq o)$
73	30	ad2antrr	$⊢ ((((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \land y \subseteq o) \to F \in Fil (X)$
74		simplrl	$⊢ ((((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \land y \subseteq o) \to y \in F$
75		elssuni	$⊢ o \in J \to o \subseteq ⋃ J$
76	75 1	sseqtrrdi	$⊢ o \in J \to o \subseteq X$
77	76	ad2antrl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to o \subseteq X$
78	77	ad2antrr	$⊢ ((((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \land y \subseteq o) \to o \subseteq X$
79		simpr	$⊢ ((((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \land y \subseteq o) \to y \subseteq o$
80		filss	$⊢ (F \in Fil (X) \land (y \in F \land o \subseteq X \land y \subseteq o)) \to o \in F$
81	73 74 78 79 80	syl13anc	$⊢ ((((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \land y \subseteq o) \to o \in F$
82	81	ex	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to (y \subseteq o \to o \in F)$
83	72 82	sylbid	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to (y \cap X \subseteq o \to o \in F)$
84	65 83	biimtrrid	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to (y \cap (X ∖ o) = \emptyset \to o \in F)$
85	84	necon3bd	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to (\neg o \in F \to y \cap (X ∖ o) \neq \emptyset)$
86	64 85	mpd	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to y \cap (X ∖ o) \neq \emptyset$
87		ssn0	$⊢ (y \cap (X ∖ o) \subseteq y \cap z \land y \cap (X ∖ o) \neq \emptyset) \to y \cap z \neq \emptyset$
88	62 86 87	syl2anc	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land (y \in F \land z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\})) \to y \cap z \neq \emptyset$
89	88	ralrimivva	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to \forall y \in F \forall z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\} y \cap z \neq \emptyset$
90		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
91	30 90	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to F \in fBas (X)$
92	48	a1i	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X ∖ o \subseteq X$
93		filtop	$⊢ F \in Fil (X) \to X \in F$
94	30 93	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X \in F$
95		eleq1	$⊢ o = X \to (o \in F \leftrightarrow X \in F)$
96	94 95	syl5ibrcom	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (o = X \to o \in F)$
97	96	necon3bd	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (\neg o \in F \to o \neq X)$
98	63 97	mpd	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to o \neq X$
99		pssdifn0	$⊢ (o \subseteq X \land o \neq X) \to X ∖ o \neq \emptyset$
100	77 98 99	syl2anc	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X ∖ o \neq \emptyset$
101		supfil	$⊢ (X \in J \land X ∖ o \subseteq X \land X ∖ o \neq \emptyset) \to \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in Fil (X)$
102	33 92 100 101	syl3anc	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in Fil (X)$
103		filfbas	$⊢ \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in Fil (X) \to \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in fBas (X)$
104	102 103	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in fBas (X)$
105		fbunfip	$⊢ (F \in fBas (X) \land \{x \in 𝒫 X \| X ∖ o \subseteq x\} \in fBas (X)) \to (\neg \emptyset \in fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \leftrightarrow \forall y \in F \forall z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\} y \cap z \neq \emptyset)$
106	91 104 105	syl2anc	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (\neg \emptyset \in fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \leftrightarrow \forall y \in F \forall z \in \{x \in 𝒫 X \| X ∖ o \subseteq x\} y \cap z \neq \emptyset)$
107	89 106	mpbird	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to \neg \emptyset \in fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})$
108		fsubbas	$⊢ X \in F \to (fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \in fBas (X) \leftrightarrow (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq 𝒫 X \land F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))$
109	94 108	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \in fBas (X) \leftrightarrow (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq 𝒫 X \land F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))$
110	45 56 107 109	mpbir3and	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \in fBas (X)$
111		ssfg	$⊢ fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \in fBas (X) \to fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \subseteq X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})$
112	110 111	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \subseteq X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})$
113	40 112	sstrd	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\} \subseteq X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})$
114	113	unssad	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to F \subseteq X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})$
115		fgcl	$⊢ fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \in fBas (X) \to X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \in Fil (X)$
116	110 115	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \in Fil (X)$
117		sseq2	$⊢ g = X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \to (F \subseteq g \leftrightarrow F \subseteq X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}))$
118		oveq2	$⊢ g = X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \to J fClus g = J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}))$
119	118	eleq2d	$⊢ g = X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \to (A \in (J fClus g) \leftrightarrow A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}))))$
120	117 119	imbi12d	$⊢ g = X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \to ((F \subseteq g \to A \in (J fClus g)) \leftrightarrow (F \subseteq X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \to A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))))$
121	120	rspcv	$⊢ X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \in Fil (X) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to (F \subseteq X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \to A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))))$
122	116 121	syl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to (F \subseteq X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}) \to A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))))$
123	114 122	mpid	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}))))$
124		simpr	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))) \to A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))$
125		simplrl	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))) \to o \in J$
126		simprrl	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to A \in o$
127	126	adantr	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))) \to A \in o$
128	113 55	sseldd	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to X ∖ o \in (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}))$
129	128	adantr	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))) \to X ∖ o \in (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}))$
130		fclsopni	$⊢ (A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}))) \land (o \in J \land A \in o \land X ∖ o \in (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))) \to o \cap (X ∖ o) \neq \emptyset$
131	124 125 127 129 130	syl13anc	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \land A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\})))) \to o \cap (X ∖ o) \neq \emptyset$
132	131	ex	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (A \in (J fClus (X filGen fi (F \cup \{x \in 𝒫 X \| X ∖ o \subseteq x\}))) \to o \cap (X ∖ o) \neq \emptyset)$
133	123 132	syld	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to o \cap (X ∖ o) \neq \emptyset)$
134	133	necon2bd	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to (o \cap (X ∖ o) = \emptyset \to \neg \forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)))$
135	29 134	mpi	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land (o \in J \land (A \in o \land \neg o \in F))) \to \neg \forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g))$
136	135	anassrs	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land o \in J) \land (A \in o \land \neg o \in F)) \to \neg \forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g))$
137	136	expr	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land o \in J) \land A \in o) \to (\neg o \in F \to \neg \forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)))$
138	137	con4d	$⊢ (((F \in Fil (X) \land (J \in Top \land A \in X)) \land o \in J) \land A \in o) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to o \in F)$
139	138	ex	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land o \in J) \to (A \in o \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to o \in F))$
140	139	com23	$⊢ ((F \in Fil (X) \land (J \in Top \land A \in X)) \land o \in J) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to (A \in o \to o \in F))$
141	140	ralrimdva	$⊢ (F \in Fil (X) \land (J \in Top \land A \in X)) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to \forall o \in J (A \in o \to o \in F))$
142		simprr	$⊢ (F \in Fil (X) \land (J \in Top \land A \in X)) \to A \in X$
143	141 142	jctild	$⊢ (F \in Fil (X) \land (J \in Top \land A \in X)) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to (A \in X \land \forall o \in J (A \in o \to o \in F)))$
144		simprl	$⊢ (F \in Fil (X) \land (J \in Top \land A \in X)) \to J \in Top$
145	144 4	sylib	$⊢ (F \in Fil (X) \land (J \in Top \land A \in X)) \to J \in TopOn (X)$
146		simpl	$⊢ (F \in Fil (X) \land (J \in Top \land A \in X)) \to F \in Fil (X)$
147		flimopn	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to o \in F)))$
148	145 146 147	syl2anc	$⊢ (F \in Fil (X) \land (J \in Top \land A \in X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to o \in F)))$
149	143 148	sylibrd	$⊢ (F \in Fil (X) \land (J \in Top \land A \in X)) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to A \in (J fLim F))$
150	149	ex	$⊢ F \in Fil (X) \to ((J \in Top \land A \in X) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to A \in (J fLim F)))$
151	150	com23	$⊢ F \in Fil (X) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to ((J \in Top \land A \in X) \to A \in (J fLim F)))$
152	28 151	mpdd	$⊢ F \in Fil (X) \to (\forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)) \to A \in (J fLim F))$
153	15 152	impbid2	$⊢ F \in Fil (X) \to (A \in (J fLim F) \leftrightarrow \forall g \in Fil (X) (F \subseteq g \to A \in (J fClus g)))$

Metamath Proof Explorer

Theorem flimfnfcls

Proof