Theorem flimfnfcls 23087

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 23086, 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 23085	. . . . 5 ⊢ (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2		flimtop 23024	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3		flimfnfcls.x	. . . . . . . . . 10 ⊢ 𝑋 = ∪ 𝐽
4	3	toptopon 21974	. . . . . . . . 9 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
5	2, 4	sylib 217	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
6	5	ad2antrr 722	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐽 ∈ (TopOn‘𝑋))
7		simplr 765	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝑔 ∈ (Fil‘𝑋))
8		simpr 484	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐹 ⊆ 𝑔)
9		flimss2 23031	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
10	6, 7, 8, 9	syl3anc 1369	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11		simpll 763	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
12	10, 11	sseldd 3918	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
13	1, 12	sselid 3915	. . . 4 ⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
14	13	ex 412	. . 3 ⊢ ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
15	14	ralrimiva 3107	. 2 ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))
16		sseq2 3943	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹))
17		oveq2 7263	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
18	17	eleq2d 2824	. . . . . 6 ⊢ (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
19	16, 18	imbi12d 344	. . . . 5 ⊢ (𝑔 = 𝐹 → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
20	19	rspcv 3547	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹))))
21		ssid 3939	. . . . . 6 ⊢ 𝐹 ⊆ 𝐹
22		id 22	. . . . . 6 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)))
23	21, 22	mpi 20	. . . . 5 ⊢ ((𝐹 ⊆ 𝐹 → 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24		fclstop 23070	. . . . . 6 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
25	3	fclselbas 23075	. . . . . 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 4402	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∩ (𝑋 ∖ 𝑜)) = ∅
30		simpll 763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31		simplrl 773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐽 ∈ Top)
32	3	topopn 21963	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
33	31, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐽)
34		pwexg 5296	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
35		rabexg 5250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
36	33, 34, 35	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V)
37		unexg 7577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
38	30, 36, 37	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V)
39		ssfii 9108	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
41		filsspw 22910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42		ssrab2 4009	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
44	41, 43	unssd 4116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
45	44	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46		ssun2 4103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
47		sseq2 3943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑋 ∖ 𝑜) → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)))
48		difss 4062	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ 𝑋
49		elpw2g 5263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ∈ 𝐽 → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
50	33, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((𝑋 ∖ 𝑜) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑋))
51	48, 50	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ 𝒫 𝑋)
52		ssid 3939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜)
53	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ (𝑋 ∖ 𝑜))
54	47, 51, 53	elrabd 3619	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})
55	46, 54	sselid 3915	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))
56	55	ne0d 4266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅)
57		sseq2 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → ((𝑋 ∖ 𝑜) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑜) ⊆ 𝑧))
58	57	elrab 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑧))
59	58	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} → (𝑋 ∖ 𝑜) ⊆ 𝑧)
60	59	ad2antll 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑋 ∖ 𝑜) ⊆ 𝑧)
61		sslin 4165	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧))
63		simprrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ 𝑜 ∈ 𝐹)
64	63	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ¬ 𝑜 ∈ 𝐹)
65		inssdif0 4300	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅)
66		simplll 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
67		simprl 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ∈ 𝐹)
68		filelss 22911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
69	66, 67, 68	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → 𝑦 ⊆ 𝑋)
70		df-ss 3900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ⊆ 𝑋 ↔ (𝑦 ∩ 𝑋) = 𝑦)
71	69, 70	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑋) = 𝑦)
72	71	sseq1d 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 ↔ 𝑦 ⊆ 𝑜))
73	30	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝐹 ∈ (Fil‘𝑋))
74		simplrl 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ∈ 𝐹)
75		elssuni 4868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ ∪ 𝐽)
76	75, 3	sseqtrrdi 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑜 ∈ 𝐽 → 𝑜 ⊆ 𝑋)
77	76	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ⊆ 𝑋)
78	77	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ⊆ 𝑋)
79		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑦 ⊆ 𝑜)
80		filss 22912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑜 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑜)) → 𝑜 ∈ 𝐹)
81	73, 74, 78, 79, 80	syl13anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∧ 𝑦 ⊆ 𝑜) → 𝑜 ∈ 𝐹)
82	81	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ⊆ 𝑜 → 𝑜 ∈ 𝐹))
83	72, 82	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ 𝑋) ⊆ 𝑜 → 𝑜 ∈ 𝐹))
84	65, 83	syl5bir 242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋 ∖ 𝑜)) = ∅ → 𝑜 ∈ 𝐹))
85	84	necon3bd 2956	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (¬ 𝑜 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅))
86	64, 85	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
87		ssn0 4331	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∩ (𝑋 ∖ 𝑜)) ⊆ (𝑦 ∩ 𝑧) ∧ (𝑦 ∩ (𝑋 ∖ 𝑜)) ≠ ∅) → (𝑦 ∩ 𝑧) ≠ ∅)
88	62, 86, 87	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ (𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) → (𝑦 ∩ 𝑧) ≠ ∅)
89	88	ralrimivva 3114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅)
90		filfbas 22907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
91	30, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ∈ (fBas‘𝑋))
92	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ⊆ 𝑋)
93		filtop 22914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
94	30, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑋 ∈ 𝐹)
95		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑜 = 𝑋 → (𝑜 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
96	94, 95	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑜 = 𝑋 → 𝑜 ∈ 𝐹))
97	96	necon3bd 2956	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (¬ 𝑜 ∈ 𝐹 → 𝑜 ≠ 𝑋))
98	63, 97	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝑜 ≠ 𝑋)
99		pssdifn0 4296	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑜 ⊆ 𝑋 ∧ 𝑜 ≠ 𝑋) → (𝑋 ∖ 𝑜) ≠ ∅)
100	77, 98, 99	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ≠ ∅)
101		supfil 22954	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑋 ∖ 𝑜) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
102	33, 92, 100, 101	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
103		filfbas 22907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105		fbunfip 22928	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅))
106	91, 104, 105	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥} (𝑦 ∩ 𝑧) ≠ ∅))
107	89, 106	mpbird 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))
108		fsubbas 22926	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
109	94, 108	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
110	45, 56, 107, 109	mpbir3and 1340	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
111		ssfg 22931	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
112	110, 111	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
113	40, 112	sstrd 3927	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
114	113	unssad 4117	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
115		fgcl 22937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
116	110, 115	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
117		sseq2 3943	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
118		oveq2 7263	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))
119	118	eleq2d 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))))
120	117, 119	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → ((𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))))))
121	120	rspcv 3547	. . . . . . . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝑜 ∈ 𝐽)
126		simprrl 777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → 𝐴 ∈ 𝑜)
127	126	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ 𝑜)
128	113, 55	sseldd 3918	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
129	128	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) ∧ (𝑜 ∈ 𝐽 ∧ (𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))
130		fclsopni 23074	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥})))) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ∧ (𝑋 ∖ 𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋 ∖ 𝑜)) ≠ ∅)
131	124, 125, 127, 129, 130	syl13anc 1370	. . . . . . . . . . . . . . . . 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 2958	. . . . . . . . . . . . . 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 3112	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹)))
142		simprr 769	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐴 ∈ 𝑋)
143	141, 142	jctild 525	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
144		simprl 767	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ Top)
145	144, 4	sylib 217	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
146		simpl 482	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → 𝐹 ∈ (Fil‘𝑋))
147		flimopn 23034	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
148	145, 146, 147	syl2anc 583	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹))))
149	143, 148	sylibrd 258	. . . . 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 225	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  {crab 3067  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  ∪ cuni 4836  ‘cfv 6418  (class class class)co 7255  ficfi 9099  fBascfbas 20498  filGencfg 20499  Topctop 21950  TopOnctopon 21967  Filcfil 22904   fLim cflim 22993   fClus cfcls 22995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1o 8267  df-er 8456  df-en 8692  df-fin 8695  df-fi 9100  df-fbas 20507  df-fg 20508  df-top 21951  df-topon 21968  df-cld 22078  df-ntr 22079  df-cls 22080  df-nei 22157  df-fil 22905  df-flim 22998  df-fcls 23000

This theorem is referenced by:  cnpfcf  23100