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
|- ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) <-> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) )

Proof

Step Hyp Ref Expression
1 filsspw
 |-  ( F e. ( Fil ` X ) -> F C_ ~P X )
2 1 adantr
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ~P X )
3 fclstop
 |-  ( A e. ( J fClus F ) -> J e. Top )
4 3 adantl
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> J e. Top )
5 eqid
 |-  U. J = U. J
6 5 neisspw
 |-  ( J e. Top -> ( ( nei ` J ) ` { A } ) C_ ~P U. J )
7 4 6 syl
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P U. J )
8 filunibas
 |-  ( F e. ( Fil ` X ) -> U. F = X )
9 5 fclsfil
 |-  ( A e. ( J fClus F ) -> F e. ( Fil ` U. J ) )
10 filunibas
 |-  ( F e. ( Fil ` U. J ) -> U. F = U. J )
11 9 10 syl
 |-  ( A e. ( J fClus F ) -> U. F = U. J )
12 8 11 sylan9req
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> X = U. J )
13 12 pweqd
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ~P X = ~P U. J )
14 7 13 sseqtrrd
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P X )
15 2 14 unssd
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X )
16 ssun1
 |-  F C_ ( F u. ( ( nei ` J ) ` { A } ) )
17 filn0
 |-  ( F e. ( Fil ` X ) -> F =/= (/) )
18 ssn0
 |-  ( ( F C_ ( F u. ( ( nei ` J ) ` { A } ) ) /\ F =/= (/) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) )
19 16 17 18 sylancr
 |-  ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) )
20 19 adantr
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) )
21 incom
 |-  ( y i^i x ) = ( x i^i y )
22 fclsneii
 |-  ( ( A e. ( J fClus F ) /\ y e. ( ( nei ` J ) ` { A } ) /\ x e. F ) -> ( y i^i x ) =/= (/) )
23 21 22 eqnetrrid
 |-  ( ( A e. ( J fClus F ) /\ y e. ( ( nei ` J ) ` { A } ) /\ x e. F ) -> ( x i^i y ) =/= (/) )
24 23 3com23
 |-  ( ( A e. ( J fClus F ) /\ x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( x i^i y ) =/= (/) )
25 24 3expb
 |-  ( ( A e. ( J fClus F ) /\ ( x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) ) -> ( x i^i y ) =/= (/) )
26 25 adantll
 |-  ( ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) /\ ( x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) ) -> ( x i^i y ) =/= (/) )
27 26 ralrimivva
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) )
28 filfbas
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
29 28 adantr
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F e. ( fBas ` X ) )
30 istopon
 |-  ( J e. ( TopOn ` X ) <-> ( J e. Top /\ X = U. J ) )
31 4 12 30 sylanbrc
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> J e. ( TopOn ` X ) )
32 5 fclselbas
 |-  ( A e. ( J fClus F ) -> A e. U. J )
33 32 adantl
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. U. J )
34 33 12 eleqtrrd
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. X )
35 34 snssd
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> { A } C_ X )
36 snnzg
 |-  ( A e. ( J fClus F ) -> { A } =/= (/) )
37 36 adantl
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> { A } =/= (/) )
38 neifil
 |-  ( ( J e. ( TopOn ` X ) /\ { A } C_ X /\ { A } =/= (/) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
39 31 35 37 38 syl3anc
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
40 filfbas
 |-  ( ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) )
41 39 40 syl
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) )
42 fbunfip
 |-  ( ( F e. ( fBas ` X ) /\ ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) <-> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) ) )
43 29 41 42 syl2anc
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) <-> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) ) )
44 27 43 mpbird
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
45 filtop
 |-  ( F e. ( Fil ` X ) -> X e. F )
46 fsubbas
 |-  ( X e. F -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
47 45 46 syl
 |-  ( F e. ( Fil ` X ) -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
48 47 adantr
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
49 15 20 44 48 mpbir3and
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) )
50 fgcl
 |-  ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) )
51 49 50 syl
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) )
52 fvex
 |-  ( ( nei ` J ) ` { A } ) e. _V
53 unexg
 |-  ( ( F e. ( Fil ` X ) /\ ( ( nei ` J ) ` { A } ) e. _V ) -> ( F u. ( ( nei ` J ) ` { A } ) ) e. _V )
54 52 53 mpan2
 |-  ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) e. _V )
55 ssfii
 |-  ( ( F u. ( ( nei ` J ) ` { A } ) ) e. _V -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
56 54 55 syl
 |-  ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
57 56 adantr
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
58 57 unssad
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
59 ssfg
 |-  ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) )
60 49 59 syl
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) )
61 58 60 sstrd
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) )
62 57 unssbd
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
63 62 60 sstrd
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) )
64 elflim
 |-  ( ( J e. ( TopOn ` X ) /\ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) ) -> ( A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) )
65 31 51 64 syl2anc
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) )
66 34 63 65 mpbir2and
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
67 sseq2
 |-  ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( F C_ g <-> F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
68 oveq2
 |-  ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( J fLim g ) = ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
69 68 eleq2d
 |-  ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( A e. ( J fLim g ) <-> A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) )
70 67 69 anbi12d
 |-  ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( ( F C_ g /\ A e. ( J fLim g ) ) <-> ( F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) )
71 70 rspcev
 |-  ( ( ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) /\ ( F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) )
72 51 61 66 71 syl12anc
 |-  ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) )
73 72 ex
 |-  ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) )
74 simprl
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> g e. ( Fil ` X ) )
75 simprrr
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fLim g ) )
76 flimtopon
 |-  ( A e. ( J fLim g ) -> ( J e. ( TopOn ` X ) <-> g e. ( Fil ` X ) ) )
77 75 76 syl
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> ( J e. ( TopOn ` X ) <-> g e. ( Fil ` X ) ) )
78 74 77 mpbird
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> J e. ( TopOn ` X ) )
79 simpl
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> F e. ( Fil ` X ) )
80 simprrl
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> F C_ g )
81 fclsss2
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ F C_ g ) -> ( J fClus g ) C_ ( J fClus F ) )
82 78 79 80 81 syl3anc
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> ( J fClus g ) C_ ( J fClus F ) )
83 flimfcls
 |-  ( J fLim g ) C_ ( J fClus g )
84 83 75 sselid
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fClus g ) )
85 82 84 sseldd
 |-  ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fClus F ) )
86 85 rexlimdvaa
 |-  ( F e. ( Fil ` X ) -> ( E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) -> A e. ( J fClus F ) ) )
87 73 86 impbid
 |-  ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) <-> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) )