This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fclsfnflim

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)

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

Proof

Step Hyp Ref Expression
1 filsspw ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
2 1 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐹 ⊆ 𝒫 𝑋 )
3 fclstop ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐽 ∈ Top )
4 3 adantl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐽 ∈ Top )
5 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
6 5 neisspw ⊢ ( 𝐽 ∈ Top → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝒫 ∪ 𝐽 )
7 4 6 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝒫 ∪ 𝐽 )
8 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
9 5 fclsfil ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
10 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) → ∪ 𝐹 = ∪ 𝐽 )
11 9 10 syl ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ∪ 𝐹 = ∪ 𝐽 )
12 8 11 sylan9req ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝑋 = ∪ 𝐽 )
13 12 pweqd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝒫 𝑋 = 𝒫 ∪ 𝐽 )
14 7 13 sseqtrrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝒫 𝑋 )
15 2 14 unssd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ⊆ 𝒫 𝑋 )
16 ssun1 ⊢ 𝐹 ⊆ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
17 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
18 ssn0 ⊢ ( ( 𝐹 ⊆ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∧ 𝐹 ≠ ∅ ) → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ≠ ∅ )
19 16 17 18 sylancr ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ≠ ∅ )
20 19 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ≠ ∅ )
21 incom ⊢ ( 𝑦 ∩ 𝑥 ) = ( 𝑥 ∩ 𝑦 )
22 fclsneii ⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑦 ∩ 𝑥 ) ≠ ∅ )
23 21 22 eqnetrrid ⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
24 23 3com23 ⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
25 24 3expb ⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) → ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
26 25 adantll ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) → ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
27 26 ralrimivva ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
28 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
29 28 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
30 istopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽 ) )
31 4 12 30 sylanbrc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
32 5 fclselbas ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴 ∈ ∪ 𝐽 )
33 32 adantl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐴 ∈ ∪ 𝐽 )
34 33 12 eleqtrrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐴 ∈ 𝑋 )
35 34 snssd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → { 𝐴 } ⊆ 𝑋 )
36 snnzg ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → { 𝐴 } ≠ ∅ )
37 36 adantl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → { 𝐴 } ≠ ∅ )
38 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ∧ { 𝐴 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
39 31 35 37 38 syl3anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
40 filfbas ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( fBas ‘ 𝑋 ) )
41 39 40 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( fBas ‘ 𝑋 ) )
42 fbunfip ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( fBas ‘ 𝑋 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) )
43 29 41 42 syl2anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) )
44 27 43 mpbird ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
45 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
46 fsubbas ⊢ ( 𝑋 ∈ 𝐹 → ( ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) )
47 45 46 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) )
48 47 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) )
49 15 20 44 48 mpbir3and ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ∈ ( fBas ‘ 𝑋 ) )
50 fgcl ⊢ ( ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) )
51 49 50 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) )
52 fvex ⊢ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ V
53 unexg ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ V ) → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∈ V )
54 52 53 mpan2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∈ V )
55 ssfii ⊢ ( ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ∈ V → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ⊆ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
56 54 55 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ⊆ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
57 56 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ⊆ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
58 57 unssad ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐹 ⊆ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
59 ssfg ⊢ ( ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) )
60 49 59 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) )
61 58 60 sstrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) )
62 57 unssbd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
63 62 60 sstrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) )
64 elflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) ) )
65 31 51 64 syl2anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) ) )
66 34 63 65 mpbir2and ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) )
67 sseq2 ⊢ ( 𝑔 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) → ( 𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) )
68 oveq2 ⊢ ( 𝑔 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) → ( 𝐽 fLim 𝑔 ) = ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) )
69 68 eleq2d ⊢ ( 𝑔 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ↔ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) ) )
70 67 69 anbi12d ⊢ ( 𝑔 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) → ( ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ↔ ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ∧ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) ) ) )
71 70 rspcev ⊢ ( ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ∧ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) ) ) ) ) → ∃ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) )
72 51 61 66 71 syl12anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ∃ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) )
73 72 ex ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ∃ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) )
74 simprl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → 𝑔 ∈ ( Fil ‘ 𝑋 ) )
75 simprrr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → 𝐴 ∈ ( 𝐽 fLim 𝑔 ) )
76 flimtopon ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝑔 ) → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) )
77 75 76 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) )
78 74 77 mpbird ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
79 simpl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
80 simprrl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → 𝐹 ⊆ 𝑔 )
81 fclsss2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑔 ) → ( 𝐽 fClus 𝑔 ) ⊆ ( 𝐽 fClus 𝐹 ) )
82 78 79 80 81 syl3anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → ( 𝐽 fClus 𝑔 ) ⊆ ( 𝐽 fClus 𝐹 ) )
83 flimfcls ⊢ ( 𝐽 fLim 𝑔 ) ⊆ ( 𝐽 fClus 𝑔 )
84 83 75 sselid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) )
85 82 84 sseldd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ) → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) )
86 85 rexlimdvaa ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) )
87 73 86 impbid ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∃ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) )