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 sseldi 
 |-  ( ( 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 ) ) ) )