flimfnfcls - Mathbox for Jeff Hankins

Mathbox for Jeff Hankins

< Previous Next >
Related theorems
GIF version

Theorem flimfnfcls 11727

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 11726, this theorem illustrates the duality between convergence and clustering.

**Hypotheses**
Ref	Expression
flimfnfcls.1	⊢ X = ∪J
flimfnfcls.2	⊢ Y = ∪F

**Assertion**
Ref	Expression
flimfnfcls	⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ ((fLim1 ‘J) ‘F) ↔ ∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g))))

Distinct variable groups: A,g g,F g,J g,X g,Y

**Proof of Theorem flimfnfcls**
Step	Hyp	Ref	Expression
1		flimfnfcls.1	. . . . . . . . 9 ⊢ X = ∪J
2		flimfnfcls.2	. . . . . . . . 9 ⊢ Y = ∪F
3		eqid 1518	. . . . . . . . 9 ⊢ ∪g = ∪g
4	1, 2, 3	limfilss 11682	. . . . . . . 8 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ g ∈ Fil) ⋀ X = Y ⋀ X = ∪g) ⋀ F ⊆ g ⋀ A ∈ ((fLim1 ‘J) ‘F)) → A ∈ ((fLim1 ‘J) ‘g))
5	4	3expia 841	. . . . . . 7 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ g ∈ Fil) ⋀ X = Y ⋀ X = ∪g) ⋀ F ⊆ g) → (A ∈ ((fLim1 ‘J) ‘F) → A ∈ ((fLim1 ‘J) ‘g)))
6		3simp1 794	. . . . . . . . . 10 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → J ∈ Top)
7	6	adantr 389	. . . . . . . . 9 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → J ∈ Top)
8		3simp2 795	. . . . . . . . . 10 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → F ∈ Fil)
9	8	adantr 389	. . . . . . . . 9 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → F ∈ Fil)
10		simprr 415	. . . . . . . . 9 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → g ∈ Fil)
11	7, 9, 10	3jca 825	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → (J ∈ Top ⋀ F ∈ Fil ⋀ g ∈ Fil))
12		3simp3 796	. . . . . . . . 9 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → X = Y)
13	12	adantr 389	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → X = Y)
14		simprll 11366	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → X = ∪g)
15	11, 13, 14	3jca 825	. . . . . . 7 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → ((J ∈ Top ⋀ F ∈ Fil ⋀ g ∈ Fil) ⋀ X = Y ⋀ X = ∪g))
16		simprlr 11367	. . . . . . 7 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → F ⊆ g)
17	5, 15, 16	sylanc 473	. . . . . 6 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → (A ∈ ((fLim1 ‘J) ‘F) → A ∈ ((fLim1 ‘J) ‘g)))
18	1, 3	flimfcls 11725	. . . . . . . 8 ⊢ ((J ∈ Top ⋀ g ∈ Fil ⋀ X = ∪g) → ((fLim1 ‘J) ‘g) ⊆ ((fClus ‘J) ‘g))
19	18, 7, 10, 14	syl3anc 864	. . . . . . 7 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → ((fLim1 ‘J) ‘g) ⊆ ((fClus ‘J) ‘g))
20	19	sseld 2119	. . . . . 6 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → (A ∈ ((fLim1 ‘J) ‘g) → A ∈ ((fClus ‘J) ‘g)))
21	17, 20	syld 27	. . . . 5 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((X = ∪g ⋀ F ⊆ g) ⋀ g ∈ Fil)) → (A ∈ ((fLim1 ‘J) ‘F) → A ∈ ((fClus ‘J) ‘g)))
22	21	exp32 377	. . . 4 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → ((X = ∪g ⋀ F ⊆ g) → (g ∈ Fil → (A ∈ ((fLim1 ‘J) ‘F) → A ∈ ((fClus ‘J) ‘g)))))
23	22	com24 37	. . 3 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ ((fLim1 ‘J) ‘F) → (g ∈ Fil → ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)))))
24	23	r19.21adv 1764	. 2 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ ((fLim1 ‘J) ‘F) → ∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g))))
25	2	eqeq2i 1528	. . . . . . . 8 ⊢ (X = Y ↔ X = ∪F)
26	25	biimpi 149	. . . . . . 7 ⊢ (X = Y → X = ∪F)
27	26	3ad2ant3 808	. . . . . 6 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → X = ∪F)
28		ssid 2132	. . . . . 6 ⊢ F ⊆ F
29	27, 28	jctir 291	. . . . 5 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (X = ∪F ⋀ F ⊆ F))
30		unieq 2576	. . . . . . . . . 10 ⊢ (g = F → ∪g = ∪F)
31	30	eqeq2d 1529	. . . . . . . . 9 ⊢ (g = F → (X = ∪g ↔ X = ∪F))
32		sseq2 2135	. . . . . . . . 9 ⊢ (g = F → (F ⊆ g ↔ F ⊆ F))
33	31, 32	anbi12d 631	. . . . . . . 8 ⊢ (g = F → ((X = ∪g ⋀ F ⊆ g) ↔ (X = ∪F ⋀ F ⊆ F)))
34		fveq2 3835	. . . . . . . . 9 ⊢ (g = F → ((fClus ‘J) ‘g) = ((fClus ‘J) ‘F))
35	34	eleq2d 1584	. . . . . . . 8 ⊢ (g = F → (A ∈ ((fClus ‘J) ‘g) ↔ A ∈ ((fClus ‘J) ‘F)))
36	33, 35	imbi12d 629	. . . . . . 7 ⊢ (g = F → (((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) ↔ ((X = ∪F ⋀ F ⊆ F) → A ∈ ((fClus ‘J) ‘F))))
37	36	rcla4v 1919	. . . . . 6 ⊢ (F ∈ Fil → (∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) → ((X = ∪F ⋀ F ⊆ F) → A ∈ ((fClus ‘J) ‘F))))
38	37	3ad2ant2 807	. . . . 5 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) → ((X = ∪F ⋀ F ⊆ F) → A ∈ ((fClus ‘J) ‘F))))
39	29, 38	mpid 47	. . . 4 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) → A ∈ ((fClus ‘J) ‘F)))
40	1, 2	fclselbas 11720	. . . . 5 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ ((fClus ‘J) ‘F)) → A ∈ X)
41	40	ex 371	. . . 4 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ ((fClus ‘J) ‘F) → A ∈ X))
42	39, 41	syld 27	. . 3 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) → A ∈ X))
43	1, 2	flimopn 11679	. . . . . . . . . 10 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (A ∈ ((fLim1 ‘J) ‘F) ↔ ∀o ∈ J (A ∈ o → o ∈ F)))
44	43	notbid 614	. . . . . . . . 9 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (¬ A ∈ ((fLim1 ‘J) ‘F) ↔ ¬ ∀o ∈ J (A ∈ o → o ∈ F)))
45		rexanali 1730	. . . . . . . . 9 ⊢ (∃o ∈ J (A ∈ o ⋀ ¬ o ∈ F) ↔ ¬ ∀o ∈ J (A ∈ o → o ∈ F))
46	44, 45	syl6bbr 541	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (¬ A ∈ ((fLim1 ‘J) ‘F) ↔ ∃o ∈ J (A ∈ o ⋀ ¬ o ∈ F)))
47		unieq 2576	. . . . . . . . . . . . . 14 ⊢ (g = (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) → ∪g = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
48	47	eqeq2d 1529	. . . . . . . . . . . . 13 ⊢ (g = (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) → (X = ∪g ↔ X = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))))
49		sseq2 2135	. . . . . . . . . . . . 13 ⊢ (g = (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) → (F ⊆ g ↔ F ⊆ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))))
50		fveq2 3835	. . . . . . . . . . . . . . 15 ⊢ (g = (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) → ((fClus ‘J) ‘g) = ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))))
51	50	eleq2d 1584	. . . . . . . . . . . . . 14 ⊢ (g = (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) → (A ∈ ((fClus ‘J) ‘g) ↔ A ∈ ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))))
52	51	notbid 614	. . . . . . . . . . . . 13 ⊢ (g = (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) → (¬ A ∈ ((fClus ‘J) ‘g) ↔ ¬ A ∈ ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))))
53	48, 49, 52	3anbi123d 899	. . . . . . . . . . . 12 ⊢ (g = (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) → ((X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g)) ↔ (X = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ⋀ F ⊆ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ⋀ ¬ A ∈ ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))))))
54	53	rcla4ev 1923	. . . . . . . . . . 11 ⊢ (((filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ∈ Fil ⋀ (X = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ⋀ F ⊆ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ⋀ ¬ A ∈ ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))))) → ∃g ∈ Fil (X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g)))
55	2	filusb 11074	. . . . . . . . . . . . . . . . 17 ⊢ (F ∈ Fil → Y ∈ F)
56		ne0i 2338	. . . . . . . . . . . . . . . . 17 ⊢ (Y ∈ F → F ≠ ∅)
57		ssun1 2245	. . . . . . . . . . . . . . . . . 18 ⊢ F ⊆ (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})
58		ssn0 2358	. . . . . . . . . . . . . . . . . 18 ⊢ ((F ⊆ (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ⋀ F ≠ ∅) → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ≠ ∅)
59	57, 58	mpan 699	. . . . . . . . . . . . . . . . 17 ⊢ (F ≠ ∅ → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ≠ ∅)
60	55, 56, 59	3syl 20	. . . . . . . . . . . . . . . 16 ⊢ (F ∈ Fil → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ≠ ∅)
61	60	3ad2ant2 807	. . . . . . . . . . . . . . 15 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ≠ ∅)
62	61	ad2antrr 404	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ≠ ∅)
63		ssn0 2358	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∩ (X ∖ o)) ⊆ (y ∩ z) ⋀ (y ∩ (X ∖ o)) ≠ ∅) → (y ∩ z) ≠ ∅)
64		visset 1859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ z ∈ V
65		sseq1 2134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = z → (x ⊆ X ↔ z ⊆ X))
66		sseq2 2135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = z → ((X ∖ o) ⊆ x ↔ (X ∖ o) ⊆ z))
67	65, 66	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = z → ((x ⊆ X ⋀ (X ∖ o) ⊆ x) ↔ (z ⊆ X ⋀ (X ∖ o) ⊆ z)))
68	64, 67	elab 1943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ↔ (z ⊆ X ⋀ (X ∖ o) ⊆ z))
69	68	pm3.27bi 324	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} → (X ∖ o) ⊆ z)
70	69	ad2antll 407	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) ⋀ (y ∈ F ⋀ z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) → (X ∖ o) ⊆ z)
71		sslin 2287	. . . . . . . . . . . . . . . . . . 19 ⊢ ((X ∖ o) ⊆ z → (y ∩ (X ∖ o)) ⊆ (y ∩ z))
72	70, 71	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ (((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) ⋀ (y ∈ F ⋀ z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) → (y ∩ (X ∖ o)) ⊆ (y ∩ z))
73		elssuni 2593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (y ∈ F → y ⊆ ∪F)
74	73, 2	syl6ssr 2160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (y ∈ F → y ⊆ Y)
75	74	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((X = Y ⋀ y ∈ F) → y ⊆ Y)
76		pm3.26 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((X = Y ⋀ y ∈ F) → X = Y)
77	75, 76	sseqtr4d 2150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((X = Y ⋀ y ∈ F) → y ⊆ X)
78	77	3ad2antl3 817	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ y ∈ F) → y ⊆ X)
79	78	ad2ant2rl 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → y ⊆ X)
80		reldisj 2366	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (y ⊆ X → ((y ∩ (X ∖ o)) = ∅ ↔ y ⊆ (X ∖ (X ∖ o))))
81	79, 80	syl 10	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → ((y ∩ (X ∖ o)) = ∅ ↔ y ⊆ (X ∖ (X ∖ o))))
82	1	eltopss 7815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((J ∈ Top ⋀ o ∈ J) → o ⊆ X)
83	82	3ad2antl1 815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ o ∈ J) → o ⊆ X)
84	83	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ (o ∈ J ⋀ A ∈ o)) → o ⊆ X)
85	84	ad2ant2r 409	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → o ⊆ X)
86		dfss4 2294	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (o ⊆ X ↔ (X ∖ (X ∖ o)) = o)
87	85, 86	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → (X ∖ (X ∖ o)) = o)
88	87	sseq2d 2141	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → (y ⊆ (X ∖ (X ∖ o)) ↔ y ⊆ o))
89	2	fillsb 11073	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (F ∈ Fil → ((y ∈ F ⋀ o ⊆ Y ⋀ y ⊆ o) → o ∈ F))
90	8	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F) ⋀ y ⊆ o)) → F ∈ Fil)
91		simprlr 11367	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F) ⋀ y ⊆ o)) → y ∈ F)
92	84	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → o ⊆ X)
93	92	ad2ant2r 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F) ⋀ y ⊆ o)) → o ⊆ X)
94	12	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F) ⋀ y ⊆ o)) → X = Y)
95	93, 94	sseqtrd 2149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F) ⋀ y ⊆ o)) → o ⊆ Y)
96		simprr 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F) ⋀ y ⊆ o)) → y ⊆ o)
97	91, 95, 96	3jca 825	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F) ⋀ y ⊆ o)) → (y ∈ F ⋀ o ⊆ Y ⋀ y ⊆ o))
98	89, 90, 97	sylc 68	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F) ⋀ y ⊆ o)) → o ∈ F)
99	98	expr 11361	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → (y ⊆ o → o ∈ F))
100	88, 99	sylbid 201	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → (y ⊆ (X ∖ (X ∖ o)) → o ∈ F))
101	81, 100	sylbid 201	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → ((y ∩ (X ∖ o)) = ∅ → o ∈ F))
102	101	necon3bd 1646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ ((o ∈ J ⋀ A ∈ o) ⋀ y ∈ F)) → (¬ o ∈ F → (y ∩ (X ∖ o)) ≠ ∅))
103	102	exp44 385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (o ∈ J → (A ∈ o → (y ∈ F → (¬ o ∈ F → (y ∩ (X ∖ o)) ≠ ∅)))))
104	103	com45 11325	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (o ∈ J → (A ∈ o → (¬ o ∈ F → (y ∈ F → (y ∩ (X ∖ o)) ≠ ∅)))))
105	104	imp55 11345	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) ⋀ y ∈ F) → (y ∩ (X ∖ o)) ≠ ∅)
106	105	adantrr 395	. . . . . . . . . . . . . . . . . 18 ⊢ (((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) ⋀ (y ∈ F ⋀ z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) → (y ∩ (X ∖ o)) ≠ ∅)
107	63, 72, 106	sylanc 473	. . . . . . . . . . . . . . . . 17 ⊢ (((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) ⋀ (y ∈ F ⋀ z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) → (y ∩ z) ≠ ∅)
108	107	ex 371	. . . . . . . . . . . . . . . 16 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ((y ∈ F ⋀ z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) → (y ∩ z) ≠ ∅))
109	108	r19.21aivv 1766	. . . . . . . . . . . . . . 15 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ∀y ∈ F ∀z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} (y ∩ z) ≠ ∅)
110		fbunfip 11631	. . . . . . . . . . . . . . . 16 ⊢ ((F ∈ fBas ⋀ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ fBas) → (∅ ∉ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ↔ ∀y ∈ F ∀z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} (y ∩ z) ≠ ∅))
111		filfbas 11628	. . . . . . . . . . . . . . . . . 18 ⊢ (F ∈ Fil → F ∈ fBas)
112	111	3ad2ant2 807	. . . . . . . . . . . . . . . . 17 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → F ∈ fBas)
113	112	ad2antrr 404	. . . . . . . . . . . . . . . 16 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → F ∈ fBas)
114		supfil 11645	. . . . . . . . . . . . . . . . . . 19 ⊢ ((X ∈ V ⋀ (X ∖ o) ⊆ X ⋀ (X ∖ o) ≠ ∅) → ({x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ Fil ⋀ X = ∪{x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))
115	114	pm3.26d 319	. . . . . . . . . . . . . . . . . 18 ⊢ ((X ∈ V ⋀ (X ∖ o) ⊆ X ⋀ (X ∖ o) ≠ ∅) → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ Fil)
116		uniexg 3094	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (J ∈ Top → ∪J ∈ V)
117	116, 1	syl5eqel 1595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (J ∈ Top → X ∈ V)
118	117	3ad2ant1 806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → X ∈ V)
119	118	ad2antrr 404	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → X ∈ V)
120		difss 2219	. . . . . . . . . . . . . . . . . . 19 ⊢ (X ∖ o) ⊆ X
121	120	a1i 8	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (X ∖ o) ⊆ X)
122	83	ad2ant2r 409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ A ∈ o)) → o ⊆ X)
123	122, 86	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ A ∈ o)) → (X ∖ (X ∖ o)) = o)
124	123	eqeq1d 1526	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ A ∈ o)) → ((X ∖ (X ∖ o)) = X ↔ o = X))
125		eleq1 1577	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (o = X → (o ∈ F ↔ X ∈ F))
126		eleq1 1577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (X = Y → (X ∈ F ↔ Y ∈ F))
127	126, 55	syl5cbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (F ∈ Fil → (X = Y → X ∈ F))
128	127	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((F ∈ Fil ⋀ X = Y) → X ∈ F)
129	128	3adant1 803	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → X ∈ F)
130	129	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ A ∈ o)) → X ∈ F)
131	125, 130	syl5cbir 209	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ A ∈ o)) → (o = X → o ∈ F))
132	124, 131	sylbid 201	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ A ∈ o)) → ((X ∖ (X ∖ o)) = X → o ∈ F))
133		difeq2 2206	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((X ∖ o) = ∅ → (X ∖ (X ∖ o)) = (X ∖ ∅))
134		dif0 2388	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (X ∖ ∅) = X
135	133, 134	syl6eq 1566	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((X ∖ o) = ∅ → (X ∖ (X ∖ o)) = X)
136	132, 135	syl5 21	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ A ∈ o)) → ((X ∖ o) = ∅ → o ∈ F))
137	136	necon3bd 1646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ A ∈ o)) → (¬ o ∈ F → (X ∖ o) ≠ ∅))
138	137	expr 11361	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ o ∈ J) → (A ∈ o → (¬ o ∈ F → (X ∖ o) ≠ ∅)))
139	138	imp3a 359	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ o ∈ J) → ((A ∈ o ⋀ ¬ o ∈ F) → (X ∖ o) ≠ ∅))
140	139	impr 11359	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (X ∖ o) ≠ ∅)
141	115, 119, 121, 140	syl3anc 864	. . . . . . . . . . . . . . . . 17 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ Fil)
142		filfbas 11628	. . . . . . . . . . . . . . . . 17 ⊢ ({x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ Fil → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ fBas)
143	141, 142	syl 10	. . . . . . . . . . . . . . . 16 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ fBas)
144	110, 113, 143	sylanc 473	. . . . . . . . . . . . . . 15 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (∅ ∉ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ↔ ∀y ∈ F ∀z ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} (y ∩ z) ≠ ∅))
145	109, 144	mpbird 194	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ∅ ∉ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))
146	62, 145	jca 286	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ((F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ≠ ∅ ⋀ ∅ ∉ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
147		unexg 3097	. . . . . . . . . . . . . . 15 ⊢ ((F ∈ Fil ⋀ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ V) → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ∈ V)
148	8	ad2antrr 404	. . . . . . . . . . . . . . 15 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → F ∈ Fil)
149		abssexg 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (X ∈ V → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ V)
150	117, 149	syl 10	. . . . . . . . . . . . . . . . 17 ⊢ (J ∈ Top → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ V)
151	150	3ad2ant1 806	. . . . . . . . . . . . . . . 16 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ V)
152	151	ad2antrr 404	. . . . . . . . . . . . . . 15 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ∈ V)
153	147, 148, 152	sylanc 473	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ∈ V)
154		fsubbas 11630	. . . . . . . . . . . . . 14 ⊢ ((F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ∈ V → ((fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ∈ fBas ↔ ((F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ≠ ∅ ⋀ ∅ ∉ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))))
155	153, 154	syl 10	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ((fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ∈ fBas ↔ ((F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ≠ ∅ ⋀ ∅ ∉ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))))
156	146, 155	mpbird 194	. . . . . . . . . . . 12 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ∈ fBas)
157		fgfil 11638	. . . . . . . . . . . 12 ⊢ ((fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ∈ fBas → (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ∈ Fil)
158	156, 157	syl 10	. . . . . . . . . . 11 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ∈ Fil)
159	12	ad2antrr 404	. . . . . . . . . . . . . . . 16 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → X = Y)
160	159, 2	syl6eq 1566	. . . . . . . . . . . . . . 15 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → X = ∪F)
161	114	pm3.27d 323	. . . . . . . . . . . . . . . 16 ⊢ ((X ∈ V ⋀ (X ∖ o) ⊆ X ⋀ (X ∖ o) ≠ ∅) → X = ∪{x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})
162	161, 119, 121, 140	syl3anc 864	. . . . . . . . . . . . . . 15 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → X = ∪{x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})
163	160, 162	uneq12d 2237	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (X ∪ X) = (∪F ∪ ∪{x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))
164		unidm 2227	. . . . . . . . . . . . . . 15 ⊢ (X ∪ X) = X
165	164	eqcomi 1522	. . . . . . . . . . . . . 14 ⊢ X = (X ∪ X)
166		uniun 2586	. . . . . . . . . . . . . 14 ⊢ ∪(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) = (∪F ∪ ∪{x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})
167	163, 165, 166	3eqtr4g 1574	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → X = ∪(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))
168		fiuni 11420	. . . . . . . . . . . . . 14 ⊢ ((F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ∈ V → ∪(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) = ∪(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))
169	153, 168	syl 10	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ∪(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) = ∪(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))
170		eqid 1518	. . . . . . . . . . . . . . 15 ⊢ ∪(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) = ∪(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))
171	170	fgbas 11636	. . . . . . . . . . . . . 14 ⊢ ((fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ∈ fBas → ∪(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
172	156, 171	syl 10	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ∪(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
173	167, 169, 172	3eqtrd 1554	. . . . . . . . . . . 12 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → X = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
174	57	a1i 8	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → F ⊆ (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))
175		abfi2 10853	. . . . . . . . . . . . . . 15 ⊢ ((F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ∈ V → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ⊆ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))
176	153, 175	syl 10	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}) ⊆ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))
177	174, 176	sstrd 2126	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → F ⊆ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))
178		fbssfg 11635	. . . . . . . . . . . . . 14 ⊢ ((fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ∈ fBas → (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ⊆ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
179	156, 178	syl 10	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})) ⊆ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
180	177, 179	sstrd 2126	. . . . . . . . . . . 12 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → F ⊆ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
181		simprl 414	. . . . . . . . . . . . . . . 16 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → o ∈ J)
182		simprrl 11368	. . . . . . . . . . . . . . . 16 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → A ∈ o)
183		ineq2 2263	. . . . . . . . . . . . . . . . . . 19 ⊢ (s = (X ∖ o) → (o ∩ s) = (o ∩ (X ∖ o)))
184	183	eqeq1d 1526	. . . . . . . . . . . . . . . . . 18 ⊢ (s = (X ∖ o) → ((o ∩ s) = ∅ ↔ (o ∩ (X ∖ o)) = ∅))
185	184	rcla4ev 1923	. . . . . . . . . . . . . . . . 17 ⊢ (((X ∖ o) ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ⋀ (o ∩ (X ∖ o)) = ∅) → ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(o ∩ s) = ∅)
186		ssun2 2246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ⊆ (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})
187	186	a1i 8	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ⊆ (F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))
188	187, 176	sstrd 2126	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ⊆ (fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))
189	188, 179	sstrd 2126	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ⊆ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
190		ssid 2132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (X ∖ o) ⊆ (X ∖ o)
191	120, 190	pm3.2i 283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((X ∖ o) ⊆ X ⋀ (X ∖ o) ⊆ (X ∖ o))
192		difexg 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (X ∈ V → (X ∖ o) ∈ V)
193		sseq1 2134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x = (X ∖ o) → (x ⊆ X ↔ (X ∖ o) ⊆ X))
194		sseq2 2135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x = (X ∖ o) → ((X ∖ o) ⊆ x ↔ (X ∖ o) ⊆ (X ∖ o)))
195	193, 194	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = (X ∖ o) → ((x ⊆ X ⋀ (X ∖ o) ⊆ x) ↔ ((X ∖ o) ⊆ X ⋀ (X ∖ o) ⊆ (X ∖ o))))
196	195	elabg 1945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((X ∖ o) ∈ V → ((X ∖ o) ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ↔ ((X ∖ o) ⊆ X ⋀ (X ∖ o) ⊆ (X ∖ o))))
197	117, 192, 196	3syl 20	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (J ∈ Top → ((X ∖ o) ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ↔ ((X ∖ o) ⊆ X ⋀ (X ∖ o) ⊆ (X ∖ o))))
198	197	3ad2ant1 806	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → ((X ∖ o) ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ↔ ((X ∖ o) ⊆ X ⋀ (X ∖ o) ⊆ (X ∖ o))))
199	198	ad2antrr 404	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ((X ∖ o) ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)} ↔ ((X ∖ o) ⊆ X ⋀ (X ∖ o) ⊆ (X ∖ o))))
200	191, 199	mpbiri 192	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (X ∖ o) ∈ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})
201	189, 200	sseldd 2120	. . . . . . . . . . . . . . . . 17 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (X ∖ o) ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))
202		difdisj 2390	. . . . . . . . . . . . . . . . . 18 ⊢ (o ∩ (X ∖ o)) = ∅
203	202	a1i 8	. . . . . . . . . . . . . . . . 17 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (o ∩ (X ∖ o)) = ∅)
204	185, 201, 203	sylanc 473	. . . . . . . . . . . . . . . 16 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(o ∩ s) = ∅)
205		eleq2 1578	. . . . . . . . . . . . . . . . . 18 ⊢ (j = o → (A ∈ j ↔ A ∈ o))
206		ineq1 2262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (j = o → (j ∩ s) = (o ∩ s))
207	206	eqeq1d 1526	. . . . . . . . . . . . . . . . . . 19 ⊢ (j = o → ((j ∩ s) = ∅ ↔ (o ∩ s) = ∅))
208	207	rexbidv 1710	. . . . . . . . . . . . . . . . . 18 ⊢ (j = o → (∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅ ↔ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(o ∩ s) = ∅))
209	205, 208	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (j = o → ((A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅) ↔ (A ∈ o ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(o ∩ s) = ∅)))
210	209	rcla4ev 1923	. . . . . . . . . . . . . . . 16 ⊢ ((o ∈ J ⋀ (A ∈ o ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(o ∩ s) = ∅)) → ∃j ∈ J (A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅))
211	181, 182, 204, 210	sylan32c 11371	. . . . . . . . . . . . . . 15 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ∃j ∈ J (A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅))
212	211	a1d 12	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (A ∈ X → ∃j ∈ J (A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅)))
213		nne 1632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (j ∩ s) ≠ ∅ ↔ (j ∩ s) = ∅)
214	213	rexbii 1714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ¬ (j ∩ s) ≠ ∅ ↔ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅)
215		rexnal 1700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ¬ (j ∩ s) ≠ ∅ ↔ ¬ ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅)
216	214, 215	bitr3i 173	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅ ↔ ¬ ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅)
217	216	anbi2i 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅) ↔ (A ∈ j ⋀ ¬ ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅))
218	217	rexbii 1714	. . . . . . . . . . . . . . . . 17 ⊢ (∃j ∈ J (A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅) ↔ ∃j ∈ J (A ∈ j ⋀ ¬ ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅))
219		rexanali 1730	. . . . . . . . . . . . . . . . 17 ⊢ (∃j ∈ J (A ∈ j ⋀ ¬ ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅) ↔ ¬ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅))
220	218, 219	bitri 171	. . . . . . . . . . . . . . . 16 ⊢ (∃j ∈ J (A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅) ↔ ¬ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅))
221	220	imbi2i 183	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ X → ∃j ∈ J (A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅)) ↔ (A ∈ X → ¬ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅)))
222		imnan 240	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ X → ¬ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅)) ↔ ¬ (A ∈ X ⋀ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅)))
223	221, 222	bitri 171	. . . . . . . . . . . . . 14 ⊢ ((A ∈ X → ∃j ∈ J (A ∈ j ⋀ ∃s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) = ∅)) ↔ ¬ (A ∈ X ⋀ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅)))
224	212, 223	sylib 196	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ¬ (A ∈ X ⋀ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅)))
225		eqid 1518	. . . . . . . . . . . . . . 15 ⊢ ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))
226	1, 225	isfclus 11718	. . . . . . . . . . . . . 14 ⊢ ((J ∈ Top ⋀ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ∈ Fil ⋀ X = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))) → (A ∈ ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))) ↔ (A ∈ X ⋀ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅))))
227	6	ad2antrr 404	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → J ∈ Top)
228	226, 227, 158, 173	syl3anc 864	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (A ∈ ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))) ↔ (A ∈ X ⋀ ∀j ∈ J (A ∈ j → ∀s ∈ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))(j ∩ s) ≠ ∅))))
229	224, 228	mtbird 720	. . . . . . . . . . . 12 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ¬ A ∈ ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)})))))
230	173, 180, 229	3jca 825	. . . . . . . . . . 11 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → (X = ∪(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ⋀ F ⊆ (filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))) ⋀ ¬ A ∈ ((fClus ‘J) ‘(filGen ‘(fi ‘(F ∪ {x∣(x ⊆ X ⋀ (X ∖ o) ⊆ x)}))))))
231	54, 158, 230	sylanc 473	. . . . . . . . . 10 ⊢ ((((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) ⋀ (o ∈ J ⋀ (A ∈ o ⋀ ¬ o ∈ F))) → ∃g ∈ Fil (X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g)))
232	231	exp32 377	. . . . . . . . 9 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (o ∈ J → ((A ∈ o ⋀ ¬ o ∈ F) → ∃g ∈ Fil (X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g)))))
233	232	r19.23adv 1792	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (∃o ∈ J (A ∈ o ⋀ ¬ o ∈ F) → ∃g ∈ Fil (X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g))))
234	46, 233	sylbid 201	. . . . . . 7 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (¬ A ∈ ((fLim1 ‘J) ‘F) → ∃g ∈ Fil (X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g))))
235		df-3an 783	. . . . . . . . 9 ⊢ ((X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g)) ↔ ((X = ∪g ⋀ F ⊆ g) ⋀ ¬ A ∈ ((fClus ‘J) ‘g)))
236	235	rexbii 1714	. . . . . . . 8 ⊢ (∃g ∈ Fil (X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g)) ↔ ∃g ∈ Fil ((X = ∪g ⋀ F ⊆ g) ⋀ ¬ A ∈ ((fClus ‘J) ‘g)))
237		rexanali 1730	. . . . . . . 8 ⊢ (∃g ∈ Fil ((X = ∪g ⋀ F ⊆ g) ⋀ ¬ A ∈ ((fClus ‘J) ‘g)) ↔ ¬ ∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)))
238	236, 237	bitri 171	. . . . . . 7 ⊢ (∃g ∈ Fil (X = ∪g ⋀ F ⊆ g ⋀ ¬ A ∈ ((fClus ‘J) ‘g)) ↔ ¬ ∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)))
239	234, 238	syl6ib 210	. . . . . 6 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (¬ A ∈ ((fLim1 ‘J) ‘F) → ¬ ∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g))))
240	239	con4d 75	. . . . 5 ⊢ (((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) ⋀ A ∈ X) → (∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) → A ∈ ((fLim1 ‘J) ‘F)))
241	240	ex 371	. . . 4 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ X → (∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) → A ∈ ((fLim1 ‘J) ‘F))))
242	241	com23 32	. . 3 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) → (A ∈ X → A ∈ ((fLim1 ‘J) ‘F))))
243	42, 242	mpdd 46	. 2 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g)) → A ∈ ((fLim1 ‘J) ‘F)))
244	24, 243	impbid 519	1 ⊢ ((J ∈ Top ⋀ F ∈ Fil ⋀ X = Y) → (A ∈ ((fLim1 ‘J) ‘F) ↔ ∀g ∈ Fil ((X = ∪g ⋀ F ⊆ g) → A ∈ ((fClus ‘J) ‘g))))

Colors of variables: wff set class

Syntax hints: ¬ wn 2 → wi 3 ↔ wb 144 ⋀ wa 221 ⋀ w3a 781 = wceq 992 ∈ wcel 994 {cab 1505 ≠ wne 1628 ∉ wnel 1629 ∀wral 1691 ∃wrex 1692 Vcvv 1857 ∖ cdif 2096 ∪ cun 2097 ∩ cin 2098 ⊆ wss 2099 ∅c0 2332 ∪cuni 2569 ‘cfv 3263 Topctop 7800 ficfi 10847 Filcfil 11069 fLim1cflim1 11096 fBascfbas 11617 filGencfg 11618 fCluscfclus 11669

This theorem is referenced by: fcluscnp 11730

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-nel 1631 df-ral 1695 df-rex 1696 df-reu 1697 df-rab 1698 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-pss 2107 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-int 2601 df-iun 2635 df-iin 2636 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-opr 4023 df-oprab 4024 df-rdg 4233 df-1o 4269 df-oadd 4271 df-er 4401 df-en 4509 df-fin 4512 df-top 7804 df-cld 7873 df-ntr 7874 df-cls 7875 df-nei 7923 df-fi 10848 df-fil 11070 df-flim1 11098 df-fbas 11619 df-fg 11620 df-fclus 11673