Theorem flimfnfcls 24402

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

Hypothesis

Ref	Expression
flimfnfcls.x	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
flimfnfcls	⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))

Distinct variable groups:   𝐴,𝑔   𝑔,𝐹   𝑔,𝐽   𝑔,𝑋

Proof of Theorem flimfnfcls

Dummy variables 𝑜 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		flimfcls 24400	. . . . 5 ⊢ (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2		flimtop 24339	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3		flimfnfcls.x	. . . . . . . . . 10 ⊢ 𝑋 = ∪ 𝐽
4	3	toptopon 23290	. . . . . . . . 9 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
5	2, 4	sylib 221	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
6	5	ad2antrr 739	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐽 ∈ (TopOn‘𝑋))
7		simplr 781	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝑔 ∈ (Fil‘𝑋))
8		simpr 490	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐹 ⊆ 𝑔)
9		flimss2 24346	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
10	6, 7, 8, 9	syl3anc 1399	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11		simpll 779	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
12	10, 11	sseldd 3914	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
13	1, 12	sselid 3911	. . . 4 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
14	13	ex 418	. . 3 ⊢ ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
15	14	ralrimiva 3158	. 2 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
16		sseq2 3939	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹))
17		oveq2 7459	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
18	17	eleq2d 2850	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
19	16, 18	imbi12d 347	. . . . 5 ⊢ (𝑔 = 𝐹 → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
20	19	rspcv 3576	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
21		ssid 3935	. . . . . 6 ⊢ 𝐹 ⊆ 𝐹
22		id 23	. . . . . 6 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)))
23	21, 22	mpi 21	. . . . 5 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24		fclstop 24385	. . . . . 6 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
25	3	fclselbas 24390	. . . . . 6 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ 𝑋)
26	24, 25	jca 521	. . . . 5 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋))
27	23, 26	syl 18	. . . 4 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋))
28	20, 27	syl6 36	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)))
29		disjdif 4429	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∩ (𝑋 ∖ 𝑜)) = ∅
30		simpll 779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31		simplrl 789	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐽 ∈ Top)
32	3	topopn 23279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
33	31, 32	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐽)
34		pwexg 5347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
35		rabexg 5306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
36	33, 34, 35	3syl 19	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
37		unexg 7792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
38	30, 36, 37	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
39		ssfii 9448	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
40	38, 39	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
41		filsspw 24225	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42		ssrab2 4008	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
44	41, 43	unssd 4193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
45	44	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46		ssun2 4180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
47		sseq2 3939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑋 ∖ 𝑜) → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)))
48		difss 4075	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ 𝑋
49		elpw2g 5302	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ∈ 𝐽 → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
50	33, 49	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
51	48, 50	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ 𝒫 𝑋)
52		ssid 3935	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)
53	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜))
54	47, 51, 53	elrabd 3650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
55	46, 54	sselid 3911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))
56	55	ne0d 4291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅)
57		sseq2 3939	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑧))
58	57	elrab 3648	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑧))
59	58	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} → (𝑋 ∖ 𝑜) ⊆ 𝑧)
60	59	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑋 ∖ 𝑜) ⊆ 𝑧)
61		sslin 4142	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
62	60, 61	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
63		simprrr 794	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ 𝑜 ∈ 𝐹)
64	63	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ¬ 𝑜 ∈ 𝐹)
65		inssdif0 4325	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅)
66		simplll 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
67		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ∈ 𝐹)
68		filelss 24226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
69	66, 67, 68	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ⊆ 𝑋)
70		dfss2 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ⊆ 𝑋 ↔ (𝑦 ∩ 𝑋) = 𝑦)
71	69, 70	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑋) = 𝑦)
72	71	sseq1d 3944	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ 𝑦 ⊆ 𝑜))
73	30	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝐹 ∈ (Fil‘𝑋))
74		simplrl 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ∈ 𝐹)
75		elssuni 4904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ ∪ 𝐽)
76	75, 3	sseqtrrdi 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ 𝑋)
77	76	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ⊆ 𝑋)
78	77	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ⊆ 𝑋)
79		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ⊆ 𝑜)
80		filss 24227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑜 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑜)) → 𝑜 ∈ 𝐹)
81	73, 74, 78, 79, 80	syl13anc 1400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ∈ 𝐹)
82	81	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ⊆ 𝑜 → 𝑜 ∈ 𝐹))
83	72, 82	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 → 𝑜 ∈ 𝐹))
84	65, 83	biimtrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅ → 𝑜 ∈ 𝐹))
85	84	necon3bd 2973	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (¬ 𝑜 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
86	64, 85	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
87		ssn0 4358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧) ∧ (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅) → (𝑦 ∩ 𝑧) ≠ ∅)
88	62, 86, 87	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑧) ≠ ∅)
89	88	ralrimivva 3209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅)
90		filfbas 24222	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
91	30, 90	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (fBas‘𝑋))
92	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ 𝑋)
93		filtop 24229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
94	30, 93	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐹)
95		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑜 = 𝑋 → (𝑜 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
96	94, 95	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑜 = 𝑋 → 𝑜 ∈ 𝐹))
97	96	necon3bd 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (¬ 𝑜 ∈ 𝐹 → 𝑜 ≠ 𝑋))
98	63, 97	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ≠ 𝑋)
99		pssdifn0 4319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑜 ⊆ 𝑋 ∧ 𝑜 ≠ 𝑋) → (𝑋 ∖ 𝑜) ≠ ∅)
100	77, 98, 99	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ≠ ∅)
101		supfil 24269	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
102	33, 92, 100, 101	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
103		filfbas 24222	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
104	102, 103	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105		fbunfip 24243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅))
106	91, 104, 105	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅))
107	89, 106	mpbird 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
108		fsubbas 24241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
109	94, 108	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
110	45, 56, 107, 109	mpbir3and 1361	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
111		ssfg 24246	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
112	110, 111	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
113	40, 112	sstrd 3923	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
114	113	unssad 4194	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
115		fgcl 24252	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
116	110, 115	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
117		sseq2 3939	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
118		oveq2 7459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
119	118	eleq2d 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))))
120	117, 119	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))))
121	120	rspcv 3576	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))))
122	116, 121	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))))
123	114, 122	mpid 45	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))))
124		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
125		simplrl 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝑜 ∈ 𝐽)
126		simprrl 793	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐴 ∈ 𝑜)
127	126	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ 𝑜)
128	113, 55	sseldd 3914	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
129	128	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
130		fclsopni 24389	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ∧ (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
131	124, 125, 127, 129, 130	syl13anc 1400	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
132	131	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
133	123, 132	syld 48	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
134	133	necon2bd 2975	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((𝑜 ∩ (𝑋 ∖ 𝑜)) = ∅ → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))
135	29, 134	mpi 21	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
136	135	anassrs 473	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹)) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
137	136	expr 462	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ 𝐴 ∈ 𝑜) → (¬ 𝑜 ∈ 𝐹 → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))
138	137	con4d 116	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ 𝐴 ∈ 𝑜) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜 ∈ 𝐹))
139	138	ex 418	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) → (𝐴 ∈ 𝑜 → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜 ∈ 𝐹)))
140	139	com23 87	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹)))
141	140	ralrimdva 3166	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹)))
142		simprr 785	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐴 ∈ 𝑋)
143	141, 142	jctild 535	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
144		simprl 783	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ Top)
145	144, 4	sylib 221	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
146		simpl 488	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐹 ∈ (Fil‘𝑋))
147		flimopn 24349	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
148	145, 146, 147	syl2anc 596	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
149	143, 148	sylibrd 262	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
150	149	ex 418	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹))))
151	150	com23 87	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝐽 fLim 𝐹))))
152	28, 151	mpdd 44	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
153	15, 152	impbid2 229	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  𝒫 cpw 4560  ∪ cuni 4872  ‘cfv 6566  (class class class)co 7451  ficfi 9439  fBascfbas 21717  filGencfg 21718  Topctop 23266  TopOnctopon 23283  Filcfil 24219   fLim cflim 24308   fClus cfcls 24310

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-1o 8514  df-2o 8515  df-en 9012  df-fin 9015  df-fi 9440  df-fbas 21726  df-fg 21727  df-top 23267  df-topon 23284  df-cld 23392  df-ntr 23393  df-cls 23394  df-nei 23471  df-fil 24220  df-flim 24313  df-fcls 24315

This theorem is used by:  cnpfcf  24415