Theorem fclsfnflim 22924

Description: A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)

Assertion

Ref	Expression
fclsfnflim	⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔))))

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

Proof of Theorem fclsfnflim

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

Step	Hyp	Ref	Expression
1		filsspw 22748	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
2	1	adantr 484	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
3		fclstop 22908	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
4	3	adantl 485	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ Top)
5		eqid 2737	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
6	5	neisspw 22004	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽)
7	4, 6	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽)
8		filunibas 22778	. . . . . . . . . 10 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 = 𝑋)
9	5	fclsfil 22907	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 ∈ (Fil‘∪ 𝐽))
10		filunibas 22778	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Fil‘∪ 𝐽) → ∪ 𝐹 = ∪ 𝐽)
11	9, 10	syl 17	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → ∪ 𝐹 = ∪ 𝐽)
12	8, 11	sylan9req 2799	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝑋 = ∪ 𝐽)
13	12	pweqd 4532	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝒫 𝑋 = 𝒫 ∪ 𝐽)
14	7, 13	sseqtrrd 3942	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋)
15	2, 14	unssd 4100	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋)
16		ssun1 4086	. . . . . . . 8 ⊢ 𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴}))
17		filn0 22759	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
18		ssn0 4315	. . . . . . . 8 ⊢ ((𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
19	16, 17, 18	sylancr 590	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
20	19	adantr 484	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
21		incom 4115	. . . . . . . . . . . 12 ⊢ (𝑦 ∩ 𝑥) = (𝑥 ∩ 𝑦)
22		fclsneii 22914	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥 ∈ 𝐹) → (𝑦 ∩ 𝑥) ≠ ∅)
23	21, 22	eqnetrrid 3016	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∩ 𝑦) ≠ ∅)
24	23	3com23 1128	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥 ∩ 𝑦) ≠ ∅)
25	24	3expb 1122	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥 ∩ 𝑦) ≠ ∅)
26	25	adantll 714	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥 ∩ 𝑦) ≠ ∅)
27	26	ralrimivva 3112	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥 ∩ 𝑦) ≠ ∅)
28		filfbas 22745	. . . . . . . . 9 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
29	28	adantr 484	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
30		istopon 21809	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽))
31	4, 12, 30	sylanbrc 586	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ (TopOn‘𝑋))
32	5	fclselbas 22913	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ ∪ 𝐽)
33	32	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ ∪ 𝐽)
34	33, 12	eleqtrrd 2841	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ 𝑋)
35	34	snssd 4722	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ⊆ 𝑋)
36		snnzg 4690	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → {𝐴} ≠ ∅)
37	36	adantl 485	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ≠ ∅)
38		neifil 22777	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
39	31, 35, 37, 38	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
40		filfbas 22745	. . . . . . . . 9 ⊢ (((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
41	39, 40	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
42		fbunfip 22766	. . . . . . . 8 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥 ∩ 𝑦) ≠ ∅))
43	29, 41, 42	syl2anc 587	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥 ∩ 𝑦) ≠ ∅))
44	27, 43	mpbird 260	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
45		filtop 22752	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
46		fsubbas 22764	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
47	45, 46	syl 17	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
48	47	adantr 484	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
49	15, 20, 44, 48	mpbir3and 1344	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋))
50		fgcl 22775	. . . . 5 ⊢ ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋))
51	49, 50	syl 17	. . . 4 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋))
52		fvex 6730	. . . . . . . . 9 ⊢ ((nei‘𝐽)‘{𝐴}) ∈ V
53		unexg 7534	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ V) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V)
54	52, 53	mpan2 691	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V)
55		ssfii 9035	. . . . . . . 8 ⊢ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
56	54, 55	syl 17	. . . . . . 7 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
57	56	adantr 484	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
58	57	unssad 4101	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
59		ssfg 22769	. . . . . 6 ⊢ ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
60	49, 59	syl 17	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
61	58, 60	sstrd 3911	. . . 4 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
62	57	unssbd 4102	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
63	62, 60	sstrd 3911	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
64		elflim 22868	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
65	31, 51, 64	syl2anc 587	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
66	34, 63, 65	mpbir2and 713	. . . 4 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
67		sseq2 3927	. . . . . 6 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
68		oveq2 7221	. . . . . . 7 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐽 fLim 𝑔) = (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
69	68	eleq2d 2823	. . . . . 6 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐴 ∈ (𝐽 fLim 𝑔) ↔ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
70	67, 69	anbi12d 634	. . . . 5 ⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → ((𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))))
71	70	rspcev 3537	. . . 4 ⊢ (((𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))
72	51, 61, 66, 71	syl12anc 837	. . 3 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))
73	72	ex 416	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔))))
74		simprl 771	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝑔 ∈ (Fil‘𝑋))
75		simprrr 782	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fLim 𝑔))
76		flimtopon 22867	. . . . . . 7 ⊢ (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋)))
77	75, 76	syl 17	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋)))
78	74, 77	mpbird 260	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐽 ∈ (TopOn‘𝑋))
79		simpl 486	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹 ∈ (Fil‘𝑋))
80		simprrl 781	. . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹 ⊆ 𝑔)
81		fclsss2 22920	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹))
82	78, 79, 80, 81	syl3anc 1373	. . . 4 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹))
83		flimfcls 22923	. . . . 5 ⊢ (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
84	83, 75	sseldi 3899	. . . 4 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝑔))
85	82, 84	sseldd 3902	. . 3 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝐹))
86	85	rexlimdvaa 3204	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)) → 𝐴 ∈ (𝐽 fClus 𝐹)))
87	73, 86	impbid 215	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110   ≠ wne 2940  ∀wral 3061  ∃wrex 3062  Vcvv 3408   ∪ cun 3864   ∩ cin 3865   ⊆ wss 3866  ∅c0 4237  𝒫 cpw 4513  {csn 4541  ∪ cuni 4819  ‘cfv 6380  (class class class)co 7213  ficfi 9026  fBascfbas 20351  filGencfg 20352  Topctop 21790  TopOnctopon 21807  neicnei 21994  Filcfil 22742   fLim cflim 22831   fClus cfcls 22833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-iin 4907  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1o 8202  df-er 8391  df-en 8627  df-fin 8630  df-fi 9027  df-fbas 20360  df-fg 20361  df-top 21791  df-topon 21808  df-cld 21916  df-ntr 21917  df-cls 21918  df-nei 21995  df-fil 22743  df-flim 22836  df-fcls 22838

This theorem is referenced by:  uffclsflim  22928  cnpfcfi  22937