Theorem flimfnfcls 23891

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 23890, 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 23889	. . . . 5 ⊢ (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2		flimtop 23828	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3		flimfnfcls.x	. . . . . . . . . 10 ⊢ 𝑋 = ∪ 𝐽
4	3	toptopon 22780	. . . . . . . . 9 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
5	2, 4	sylib 218	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
6	5	ad2antrr 726	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐽 ∈ (TopOn‘𝑋))
7		simplr 768	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝑔 ∈ (Fil‘𝑋))
8		simpr 484	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐹 ⊆ 𝑔)
9		flimss2 23835	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
10	6, 7, 8, 9	syl3anc 1373	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11		simpll 766	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
12	10, 11	sseldd 3944	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
13	1, 12	sselid 3941	. . . 4 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
14	13	ex 412	. . 3 ⊢ ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
15	14	ralrimiva 3125	. 2 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
16		sseq2 3970	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹))
17		oveq2 7377	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
18	17	eleq2d 2814	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
19	16, 18	imbi12d 344	. . . . 5 ⊢ (𝑔 = 𝐹 → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
20	19	rspcv 3581	. . . 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 23874	. . . . . 6 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
25	3	fclselbas 23879	. . . . . 6 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ 𝑋)
26	24, 25	jca 511	. . . . 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 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐽 ∈ Top)
32	3	topopn 22769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
33	31, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐽)
34		pwexg 5328	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
35		rabexg 5287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
36	33, 34, 35	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
37		unexg 7699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
38	30, 36, 37	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
39		ssfii 9346	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
41		filsspw 23714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42		ssrab2 4039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
44	41, 43	unssd 4151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
45	44	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46		ssun2 4138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
47		sseq2 3970	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑋 ∖ 𝑜) → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)))
48		difss 4095	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ 𝑋
49		elpw2g 5283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ∈ 𝐽 → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
50	33, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
51	48, 50	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ 𝒫 𝑋)
52		ssid 3966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)
53	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜))
54	47, 51, 53	elrabd 3658	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
55	46, 54	sselid 3941	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))
56	55	ne0d 4301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅)
57		sseq2 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑧))
58	57	elrab 3656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑧))
59	58	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} → (𝑋 ∖ 𝑜) ⊆ 𝑧)
60	59	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑋 ∖ 𝑜) ⊆ 𝑧)
61		sslin 4202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
63		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ 𝑜 ∈ 𝐹)
64	63	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ¬ 𝑜 ∈ 𝐹)
65		inssdif0 4333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅)
66		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
67		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ∈ 𝐹)
68		filelss 23715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
69	66, 67, 68	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ⊆ 𝑋)
70		dfss2 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ⊆ 𝑋 ↔ (𝑦 ∩ 𝑋) = 𝑦)
71	69, 70	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑋) = 𝑦)
72	71	sseq1d 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ 𝑦 ⊆ 𝑜))
73	30	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝐹 ∈ (Fil‘𝑋))
74		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ∈ 𝐹)
75		elssuni 4897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ ∪ 𝐽)
76	75, 3	sseqtrrdi 3985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ 𝑋)
77	76	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ⊆ 𝑋)
78	77	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ⊆ 𝑋)
79		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ⊆ 𝑜)
80		filss 23716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑜 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑜)) → 𝑜 ∈ 𝐹)
81	73, 74, 78, 79, 80	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ∈ 𝐹)
82	81	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ⊆ 𝑜 → 𝑜 ∈ 𝐹))
83	72, 82	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 → 𝑜 ∈ 𝐹))
84	65, 83	biimtrrid 243	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅ → 𝑜 ∈ 𝐹))
85	84	necon3bd 2939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (¬ 𝑜 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
86	64, 85	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
87		ssn0 4363	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧) ∧ (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅) → (𝑦 ∩ 𝑧) ≠ ∅)
88	62, 86, 87	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑧) ≠ ∅)
89	88	ralrimivva 3178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅)
90		filfbas 23711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
91	30, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (fBas‘𝑋))
92	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ 𝑋)
93		filtop 23718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
94	30, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐹)
95		eleq1 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑜 = 𝑋 → (𝑜 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
96	94, 95	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑜 = 𝑋 → 𝑜 ∈ 𝐹))
97	96	necon3bd 2939	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (¬ 𝑜 ∈ 𝐹 → 𝑜 ≠ 𝑋))
98	63, 97	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ≠ 𝑋)
99		pssdifn0 4327	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑜 ⊆ 𝑋 ∧ 𝑜 ≠ 𝑋) → (𝑋 ∖ 𝑜) ≠ ∅)
100	77, 98, 99	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ≠ ∅)
101		supfil 23758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
102	33, 92, 100, 101	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
103		filfbas 23711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105		fbunfip 23732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅))
106	91, 104, 105	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅))
107	89, 106	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
108		fsubbas 23730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
109	94, 108	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
110	45, 56, 107, 109	mpbir3and 1343	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
111		ssfg 23735	. . . . . . . . . . . . . . . . . . . 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 4152	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
115		fgcl 23741	. . . . . . . . . . . . . . . . . . 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 7377	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
119	118	eleq2d 2814	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))))
120	117, 119	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))))
121	120	rspcv 3581	. . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
125		simplrl 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝑜 ∈ 𝐽)
126		simprrl 780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐴 ∈ 𝑜)
127	126	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ 𝑜)
128	113, 55	sseldd 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
129	128	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
130		fclsopni 23878	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ∧ (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
131	124, 125, 127, 129, 130	syl13anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
132	131	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
133	123, 132	syld 47	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
134	133	necon2bd 2941	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((𝑜 ∩ (𝑋 ∖ 𝑜)) = ∅ → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))
135	29, 134	mpi 20	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
136	135	anassrs 467	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹)) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
137	136	expr 456	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ 𝐴 ∈ 𝑜) → (¬ 𝑜 ∈ 𝐹 → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))
138	137	con4d 115	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) ∧ 𝐴 ∈ 𝑜) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜 ∈ 𝐹))
139	138	ex 412	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) → (𝐴 ∈ 𝑜 → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜 ∈ 𝐹)))
140	139	com23 86	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ 𝑜 ∈ 𝐽) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹)))
141	140	ralrimdva 3133	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹)))
142		simprr 772	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐴 ∈ 𝑋)
143	141, 142	jctild 525	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
144		simprl 770	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ Top)
145	144, 4	sylib 218	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
146		simpl 482	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐹 ∈ (Fil‘𝑋))
147		flimopn 23838	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
148	145, 146, 147	syl2anc 584	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
149	143, 148	sylibrd 259	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
150	149	ex 412	. . . 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 226	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  {crab 3402  Vcvv 3444   ∖ cdif 3908   ∪ cun 3909   ∩ cin 3910   ⊆ wss 3911  ∅c0 4292  𝒫 cpw 4559  ∪ cuni 4867  ‘cfv 6499  (class class class)co 7369  ficfi 9337  fBascfbas 21228  filGencfg 21229  Topctop 22756  TopOnctopon 22773  Filcfil 23708   fLim cflim 23797   fClus cfcls 23799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1o 8411  df-2o 8412  df-en 8896  df-fin 8899  df-fi 9338  df-fbas 21237  df-fg 21238  df-top 22757  df-topon 22774  df-cld 22882  df-ntr 22883  df-cls 22884  df-nei 22961  df-fil 23709  df-flim 23802  df-fcls 23804

This theorem is referenced by:  cnpfcf  23904