Theorem flimfnfcls 23379

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 23378, 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 23377	. . . . 5 ⊢ (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2		flimtop 23316	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3		flimfnfcls.x	. . . . . . . . . 10 ⊢ 𝑋 = ∪ 𝐽
4	3	toptopon 22266	. . . . . . . . 9 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
5	2, 4	sylib 217	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
6	5	ad2antrr 724	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐽 ∈ (TopOn‘𝑋))
7		simplr 767	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝑔 ∈ (Fil‘𝑋))
8		simpr 485	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐹 ⊆ 𝑔)
9		flimss2 23323	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
10	6, 7, 8, 9	syl3anc 1371	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11		simpll 765	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
12	10, 11	sseldd 3945	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
13	1, 12	sselid 3942	. . . 4 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
14	13	ex 413	. . 3 ⊢ ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
15	14	ralrimiva 3143	. 2 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
16		sseq2 3970	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹))
17		oveq2 7365	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
18	17	eleq2d 2823	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
19	16, 18	imbi12d 344	. . . . 5 ⊢ (𝑔 = 𝐹 → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
20	19	rspcv 3577	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
21		ssid 3966	. . . . . 6 ⊢ 𝐹 ⊆ 𝐹
22		id 22	. . . . . 6 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)))
23	21, 22	mpi 20	. . . . 5 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24		fclstop 23362	. . . . . 6 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
25	3	fclselbas 23367	. . . . . 6 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ 𝑋)
26	24, 25	jca 512	. . . . 5 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋))
27	23, 26	syl 17	. . . 4 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋))
28	20, 27	syl6 35	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)))
29		disjdif 4431	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∩ (𝑋 ∖ 𝑜)) = ∅
30		simpll 765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31		simplrl 775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐽 ∈ Top)
32	3	topopn 22255	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
33	31, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐽)
34		pwexg 5333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
35		rabexg 5288	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
36	33, 34, 35	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
37		unexg 7683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
38	30, 36, 37	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
39		ssfii 9355	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
41		filsspw 23202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42		ssrab2 4037	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
44	41, 43	unssd 4146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
45	44	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46		ssun2 4133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
47		sseq2 3970	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑋 ∖ 𝑜) → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)))
48		difss 4091	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ 𝑋
49		elpw2g 5301	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ∈ 𝐽 → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
50	33, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
51	48, 50	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ 𝒫 𝑋)
52		ssid 3966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)
53	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜))
54	47, 51, 53	elrabd 3647	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
55	46, 54	sselid 3942	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))
56	55	ne0d 4295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅)
57		sseq2 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑧))
58	57	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑧))
59	58	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} → (𝑋 ∖ 𝑜) ⊆ 𝑧)
60	59	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑋 ∖ 𝑜) ⊆ 𝑧)
61		sslin 4194	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
63		simprrr 780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ 𝑜 ∈ 𝐹)
64	63	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ¬ 𝑜 ∈ 𝐹)
65		inssdif0 4329	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅)
66		simplll 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
67		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ∈ 𝐹)
68		filelss 23203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
69	66, 67, 68	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ⊆ 𝑋)
70		df-ss 3927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ⊆ 𝑋 ↔ (𝑦 ∩ 𝑋) = 𝑦)
71	69, 70	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑋) = 𝑦)
72	71	sseq1d 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ 𝑦 ⊆ 𝑜))
73	30	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝐹 ∈ (Fil‘𝑋))
74		simplrl 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ∈ 𝐹)
75		elssuni 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ ∪ 𝐽)
76	75, 3	sseqtrrdi 3995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ 𝑋)
77	76	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ⊆ 𝑋)
78	77	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ⊆ 𝑋)
79		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ⊆ 𝑜)
80		filss 23204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑜 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑜)) → 𝑜 ∈ 𝐹)
81	73, 74, 78, 79, 80	syl13anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ∈ 𝐹)
82	81	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ⊆ 𝑜 → 𝑜 ∈ 𝐹))
83	72, 82	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 → 𝑜 ∈ 𝐹))
84	65, 83	biimtrrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅ → 𝑜 ∈ 𝐹))
85	84	necon3bd 2957	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (¬ 𝑜 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
86	64, 85	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
87		ssn0 4360	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧) ∧ (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅) → (𝑦 ∩ 𝑧) ≠ ∅)
88	62, 86, 87	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑧) ≠ ∅)
89	88	ralrimivva 3197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅)
90		filfbas 23199	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
91	30, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (fBas‘𝑋))
92	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ 𝑋)
93		filtop 23206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
94	30, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐹)
95		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑜 = 𝑋 → (𝑜 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
96	94, 95	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑜 = 𝑋 → 𝑜 ∈ 𝐹))
97	96	necon3bd 2957	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (¬ 𝑜 ∈ 𝐹 → 𝑜 ≠ 𝑋))
98	63, 97	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ≠ 𝑋)
99		pssdifn0 4325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑜 ⊆ 𝑋 ∧ 𝑜 ≠ 𝑋) → (𝑋 ∖ 𝑜) ≠ ∅)
100	77, 98, 99	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ≠ ∅)
101		supfil 23246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
102	33, 92, 100, 101	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
103		filfbas 23199	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105		fbunfip 23220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅))
106	91, 104, 105	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅))
107	89, 106	mpbird 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
108		fsubbas 23218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
109	94, 108	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
110	45, 56, 107, 109	mpbir3and 1342	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
111		ssfg 23223	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
112	110, 111	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
113	40, 112	sstrd 3954	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
114	113	unssad 4147	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
115		fgcl 23229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
116	110, 115	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
117		sseq2 3970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
118		oveq2 7365	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
119	118	eleq2d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))))
120	117, 119	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))))
121	120	rspcv 3577	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))))
122	116, 121	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))))
123	114, 122	mpid 44	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))))
124		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
125		simplrl 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝑜 ∈ 𝐽)
126		simprrl 779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐴 ∈ 𝑜)
127	126	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ 𝑜)
128	113, 55	sseldd 3945	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
129	128	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
130		fclsopni 23366	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ∧ (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
131	124, 125, 127, 129, 130	syl13anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
132	131	ex 413	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
133	123, 132	syld 47	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
134	133	necon2bd 2959	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((𝑜 ∩ (𝑋 ∖ 𝑜)) = ∅ → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))
135	29, 134	mpi 20	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
136	135	anassrs 468	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹)) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
137	136	expr 457	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ 𝐴 ∈ 𝑜) → (¬ 𝑜 ∈ 𝐹 → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))
138	137	con4d 115	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ 𝐴 ∈ 𝑜) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜 ∈ 𝐹))
139	138	ex 413	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) → (𝐴 ∈ 𝑜 → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜 ∈ 𝐹)))
140	139	com23 86	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹)))
141	140	ralrimdva 3151	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹)))
142		simprr 771	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐴 ∈ 𝑋)
143	141, 142	jctild 526	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
144		simprl 769	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ Top)
145	144, 4	sylib 217	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
146		simpl 483	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐹 ∈ (Fil‘𝑋))
147		flimopn 23326	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
148	145, 146, 147	syl2anc 584	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
149	143, 148	sylibrd 258	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
150	149	ex 413	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹))))
151	150	com23 86	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝐽 fLim 𝐹))))
152	28, 151	mpdd 43	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
153	15, 152	impbid2 225	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  {crab 3407  Vcvv 3445   ∖ cdif 3907   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  ∪ cuni 4865  ‘cfv 6496  (class class class)co 7357  ficfi 9346  fBascfbas 20784  filGencfg 20785  Topctop 22242  TopOnctopon 22259  Filcfil 23196   fLim cflim 23285   fClus cfcls 23287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1o 8412  df-er 8648  df-en 8884  df-fin 8887  df-fi 9347  df-fbas 20793  df-fg 20794  df-top 22243  df-topon 22260  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-fil 23197  df-flim 23290  df-fcls 23292

This theorem is referenced by:  cnpfcf  23392