Theorem flimfnfcls 23915

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 23914, 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 23913	. . . . 5 ⊢ (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2		flimtop 23852	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3		flimfnfcls.x	. . . . . . . . . 10 ⊢ 𝑋 = ∪ 𝐽
4	3	toptopon 22804	. . . . . . . . 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 23859	. . . . . . 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 3947	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
13	1, 12	sselid 3944	. . . 4 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
14	13	ex 412	. . 3 ⊢ ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
15	14	ralrimiva 3125	. 2 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
16		sseq2 3973	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹))
17		oveq2 7395	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
18	17	eleq2d 2814	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
19	16, 18	imbi12d 344	. . . . 5 ⊢ (𝑔 = 𝐹 → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
20	19	rspcv 3584	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
21		ssid 3969	. . . . . 6 ⊢ 𝐹 ⊆ 𝐹
22		id 22	. . . . . 6 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)))
23	21, 22	mpi 20	. . . . 5 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24		fclstop 23898	. . . . . 6 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
25	3	fclselbas 23903	. . . . . 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 4435	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∩ (𝑋 ∖ 𝑜)) = ∅
30		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐽 ∈ Top)
32	3	topopn 22793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
33	31, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐽)
34		pwexg 5333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
35		rabexg 5292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
36	33, 34, 35	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
37		unexg 7719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
38	30, 36, 37	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
39		ssfii 9370	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
41		filsspw 23738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42		ssrab2 4043	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
44	41, 43	unssd 4155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
45	44	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46		ssun2 4142	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
47		sseq2 3973	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑋 ∖ 𝑜) → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)))
48		difss 4099	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ 𝑋
49		elpw2g 5288	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ∈ 𝐽 → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
50	33, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
51	48, 50	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ 𝒫 𝑋)
52		ssid 3969	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)
53	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜))
54	47, 51, 53	elrabd 3661	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
55	46, 54	sselid 3944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))
56	55	ne0d 4305	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅)
57		sseq2 3973	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑧))
58	57	elrab 3659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑧))
59	58	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} → (𝑋 ∖ 𝑜) ⊆ 𝑧)
60	59	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑋 ∖ 𝑜) ⊆ 𝑧)
61		sslin 4206	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
63		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ 𝑜 ∈ 𝐹)
64	63	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ¬ 𝑜 ∈ 𝐹)
65		inssdif0 4337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅)
66		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
67		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ∈ 𝐹)
68		filelss 23739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
69	66, 67, 68	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ⊆ 𝑋)
70		dfss2 3932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ⊆ 𝑋 ↔ (𝑦 ∩ 𝑋) = 𝑦)
71	69, 70	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑋) = 𝑦)
72	71	sseq1d 3978	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ 𝑦 ⊆ 𝑜))
73	30	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝐹 ∈ (Fil‘𝑋))
74		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ∈ 𝐹)
75		elssuni 4901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ ∪ 𝐽)
76	75, 3	sseqtrrdi 3988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ 𝑋)
77	76	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ⊆ 𝑋)
78	77	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ⊆ 𝑋)
79		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ⊆ 𝑜)
80		filss 23740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4367	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧) ∧ (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅) → (𝑦 ∩ 𝑧) ≠ ∅)
88	62, 86, 87	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑧) ≠ ∅)
89	88	ralrimivva 3180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅)
90		filfbas 23735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
91	30, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (fBas‘𝑋))
92	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ 𝑋)
93		filtop 23742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4331	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑜 ⊆ 𝑋 ∧ 𝑜 ≠ 𝑋) → (𝑋 ∖ 𝑜) ≠ ∅)
100	77, 98, 99	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ≠ ∅)
101		supfil 23782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
102	33, 92, 100, 101	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
103		filfbas 23735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105		fbunfip 23756	. . . . . . . . . . . . . . . . . . . . . . 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 23754	. . . . . . . . . . . . . . . . . . . . . 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 23759	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
112	110, 111	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
113	40, 112	sstrd 3957	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
114	113	unssad 4156	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
115		fgcl 23765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
116	110, 115	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
117		sseq2 3973	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
118		oveq2 7395	. . . . . . . . . . . . . . . . . . . . 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 3584	. . . . . . . . . . . . . . . . . 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 3947	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
129	128	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
130		fclsopni 23902	. . . . . . . . . . . . . . . . . 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 23862	. . . . . . 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 3405  Vcvv 3447   ∖ cdif 3911   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  𝒫 cpw 4563  ∪ cuni 4871  ‘cfv 6511  (class class class)co 7387  ficfi 9361  fBascfbas 21252  filGencfg 21253  Topctop 22780  TopOnctopon 22797  Filcfil 23732   fLim cflim 23821   fClus cfcls 23823

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 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-iin 4958  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1o 8434  df-2o 8435  df-en 8919  df-fin 8922  df-fi 9362  df-fbas 21261  df-fg 21262  df-top 22781  df-topon 22798  df-cld 22906  df-ntr 22907  df-cls 22908  df-nei 22985  df-fil 23733  df-flim 23826  df-fcls 23828

This theorem is referenced by:  cnpfcf  23928