Metamath Proof Explorer

Theorem flimfnfcls

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim , this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypothesis flimfnfcls.x 
|- X = U. J
Assertion flimfnfcls 
|- ( F e. ( Fil ` X ) -> ( A e. ( J fLim F ) <-> A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) ) )

Proof

Step Hyp Ref Expression
1 flimfnfcls.x 
 |-  X = U. J
2 flimfcls 
 |-  ( J fLim g ) C_ ( J fClus g )
3 flimtop 
 |-  ( A e. ( J fLim F ) -> J e. Top )
4 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
5 3 4 sylib 
 |-  ( A e. ( J fLim F ) -> J e. ( TopOn ` X ) )
6 5 ad2antrr 
 |-  ( ( ( A e. ( J fLim F ) /\ g e. ( Fil ` X ) ) /\ F C_ g ) -> J e. ( TopOn ` X ) )
7 simplr 
 |-  ( ( ( A e. ( J fLim F ) /\ g e. ( Fil ` X ) ) /\ F C_ g ) -> g e. ( Fil ` X ) )
8 simpr 
 |-  ( ( ( A e. ( J fLim F ) /\ g e. ( Fil ` X ) ) /\ F C_ g ) -> F C_ g )
9 flimss2 
 |-  ( ( J e. ( TopOn ` X ) /\ g e. ( Fil ` X ) /\ F C_ g ) -> ( J fLim F ) C_ ( J fLim g ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( A e. ( J fLim F ) /\ g e. ( Fil ` X ) ) /\ F C_ g ) -> ( J fLim F ) C_ ( J fLim g ) )
11 simpll 
 |-  ( ( ( A e. ( J fLim F ) /\ g e. ( Fil ` X ) ) /\ F C_ g ) -> A e. ( J fLim F ) )
12 10 11 sseldd 
 |-  ( ( ( A e. ( J fLim F ) /\ g e. ( Fil ` X ) ) /\ F C_ g ) -> A e. ( J fLim g ) )
13 2 12 sselid 
 |-  ( ( ( A e. ( J fLim F ) /\ g e. ( Fil ` X ) ) /\ F C_ g ) -> A e. ( J fClus g ) )
14 13 ex 
 |-  ( ( A e. ( J fLim F ) /\ g e. ( Fil ` X ) ) -> ( F C_ g -> A e. ( J fClus g ) ) )
15 14 ralrimiva 
 |-  ( A e. ( J fLim F ) -> A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) )
16 sseq2 
 |-  ( g = F -> ( F C_ g <-> F C_ F ) )
17 oveq2 
 |-  ( g = F -> ( J fClus g ) = ( J fClus F ) )
18 17 eleq2d 
 |-  ( g = F -> ( A e. ( J fClus g ) <-> A e. ( J fClus F ) ) )
19 16 18 imbi12d 
 |-  ( g = F -> ( ( F C_ g -> A e. ( J fClus g ) ) <-> ( F C_ F -> A e. ( J fClus F ) ) ) )
20 19 rspcv 
 |-  ( F e. ( Fil ` X ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> ( F C_ F -> A e. ( J fClus F ) ) ) )
21 ssid 
 |-  F C_ F
22 id 
 |-  ( ( F C_ F -> A e. ( J fClus F ) ) -> ( F C_ F -> A e. ( J fClus F ) ) )
23 21 22 mpi 
 |-  ( ( F C_ F -> A e. ( J fClus F ) ) -> A e. ( J fClus F ) )
24 fclstop 
 |-  ( A e. ( J fClus F ) -> J e. Top )
25 1 fclselbas 
 |-  ( A e. ( J fClus F ) -> A e. X )
26 24 25 jca 
 |-  ( A e. ( J fClus F ) -> ( J e. Top /\ A e. X ) )
27 23 26 syl 
 |-  ( ( F C_ F -> A e. ( J fClus F ) ) -> ( J e. Top /\ A e. X ) )
28 20 27 syl6 
 |-  ( F e. ( Fil ` X ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> ( J e. Top /\ A e. X ) ) )
29 disjdif 
 |-  ( o i^i ( X \ o ) ) = (/)
30 simpll 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> F e. ( Fil ` X ) )
31 simplrl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> J e. Top )
32 1 topopn 
 |-  ( J e. Top -> X e. J )
33 31 32 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> X e. J )
34 pwexg 
 |-  ( X e. J -> ~P X e. _V )
35 rabexg 
 |-  ( ~P X e. _V -> { x e. ~P X | ( X \ o ) C_ x } e. _V )
36 33 34 35 3syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> { x e. ~P X | ( X \ o ) C_ x } e. _V )
37 unexg 
 |-  ( ( F e. ( Fil ` X ) /\ { x e. ~P X | ( X \ o ) C_ x } e. _V ) -> ( F u. { x e. ~P X | ( X \ o ) C_ x } ) e. _V )
38 30 36 37 syl2anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( F u. { x e. ~P X | ( X \ o ) C_ x } ) e. _V )
39 ssfii 
 |-  ( ( F u. { x e. ~P X | ( X \ o ) C_ x } ) e. _V -> ( F u. { x e. ~P X | ( X \ o ) C_ x } ) C_ ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) )
40 38 39 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( F u. { x e. ~P X | ( X \ o ) C_ x } ) C_ ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) )
41 filsspw 
 |-  ( F e. ( Fil ` X ) -> F C_ ~P X )
42 ssrab2 
 |-  { x e. ~P X | ( X \ o ) C_ x } C_ ~P X
43 42 a1i 
 |-  ( F e. ( Fil ` X ) -> { x e. ~P X | ( X \ o ) C_ x } C_ ~P X )
44 41 43 unssd 
 |-  ( F e. ( Fil ` X ) -> ( F u. { x e. ~P X | ( X \ o ) C_ x } ) C_ ~P X )
45 44 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( F u. { x e. ~P X | ( X \ o ) C_ x } ) C_ ~P X )
46 ssun2 
 |-  { x e. ~P X | ( X \ o ) C_ x } C_ ( F u. { x e. ~P X | ( X \ o ) C_ x } )
47 sseq2 
 |-  ( x = ( X \ o ) -> ( ( X \ o ) C_ x <-> ( X \ o ) C_ ( X \ o ) ) )
48 difss 
 |-  ( X \ o ) C_ X
49 elpw2g 
 |-  ( X e. J -> ( ( X \ o ) e. ~P X <-> ( X \ o ) C_ X ) )
50 33 49 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( ( X \ o ) e. ~P X <-> ( X \ o ) C_ X ) )
51 48 50 mpbiri 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( X \ o ) e. ~P X )
52 ssid 
 |-  ( X \ o ) C_ ( X \ o )
53 52 a1i 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( X \ o ) C_ ( X \ o ) )
54 47 51 53 elrabd 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( X \ o ) e. { x e. ~P X | ( X \ o ) C_ x } )
55 46 54 sselid 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( X \ o ) e. ( F u. { x e. ~P X | ( X \ o ) C_ x } ) )
56 55 ne0d 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( F u. { x e. ~P X | ( X \ o ) C_ x } ) =/= (/) )
57 sseq2 
 |-  ( x = z -> ( ( X \ o ) C_ x <-> ( X \ o ) C_ z ) )
58 57 elrab 
 |-  ( z e. { x e. ~P X | ( X \ o ) C_ x } <-> ( z e. ~P X /\ ( X \ o ) C_ z ) )
59 58 simprbi 
 |-  ( z e. { x e. ~P X | ( X \ o ) C_ x } -> ( X \ o ) C_ z )
60 59 ad2antll 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( X \ o ) C_ z )
61 sslin 
 |-  ( ( X \ o ) C_ z -> ( y i^i ( X \ o ) ) C_ ( y i^i z ) )
62 60 61 syl 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( y i^i ( X \ o ) ) C_ ( y i^i z ) )
63 simprrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> -. o e. F )
64 63 adantr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> -. o e. F )
65 inssdif0 
 |-  ( ( y i^i X ) C_ o <-> ( y i^i ( X \ o ) ) = (/) )
66 simplll 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> F e. ( Fil ` X ) )
67 simprl 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> y e. F )
68 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ y e. F ) -> y C_ X )
69 66 67 68 syl2anc 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> y C_ X )
70 df-ss 
 |-  ( y C_ X <-> ( y i^i X ) = y )
71 69 70 sylib 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( y i^i X ) = y )
72 71 sseq1d 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( ( y i^i X ) C_ o <-> y C_ o ) )
73 30 ad2antrr 
 |-  ( ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) /\ y C_ o ) -> F e. ( Fil ` X ) )
74 simplrl 
 |-  ( ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) /\ y C_ o ) -> y e. F )
75 elssuni 
 |-  ( o e. J -> o C_ U. J )
76 75 1 sseqtrrdi 
 |-  ( o e. J -> o C_ X )
77 76 ad2antrl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> o C_ X )
78 77 ad2antrr 
 |-  ( ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) /\ y C_ o ) -> o C_ X )
79 simpr 
 |-  ( ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) /\ y C_ o ) -> y C_ o )
80 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( y e. F /\ o C_ X /\ y C_ o ) ) -> o e. F )
81 73 74 78 79 80 syl13anc 
 |-  ( ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) /\ y C_ o ) -> o e. F )
82 81 ex 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( y C_ o -> o e. F ) )
83 72 82 sylbid 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( ( y i^i X ) C_ o -> o e. F ) )
84 65 83 syl5bir 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( ( y i^i ( X \ o ) ) = (/) -> o e. F ) )
85 84 necon3bd 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( -. o e. F -> ( y i^i ( X \ o ) ) =/= (/) ) )
86 64 85 mpd 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( y i^i ( X \ o ) ) =/= (/) )
87 ssn0 
 |-  ( ( ( y i^i ( X \ o ) ) C_ ( y i^i z ) /\ ( y i^i ( X \ o ) ) =/= (/) ) -> ( y i^i z ) =/= (/) )
88 62 86 87 syl2anc 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ ( y e. F /\ z e. { x e. ~P X | ( X \ o ) C_ x } ) ) -> ( y i^i z ) =/= (/) )
89 88 ralrimivva 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> A. y e. F A. z e. { x e. ~P X | ( X \ o ) C_ x } ( y i^i z ) =/= (/) )
90 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
91 30 90 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> F e. ( fBas ` X ) )
92 48 a1i 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( X \ o ) C_ X )
93 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
94 30 93 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> X e. F )
95 eleq1 
 |-  ( o = X -> ( o e. F <-> X e. F ) )
96 94 95 syl5ibrcom 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( o = X -> o e. F ) )
97 96 necon3bd 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( -. o e. F -> o =/= X ) )
98 63 97 mpd 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> o =/= X )
99 pssdifn0 
 |-  ( ( o C_ X /\ o =/= X ) -> ( X \ o ) =/= (/) )
100 77 98 99 syl2anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( X \ o ) =/= (/) )
101 supfil 
 |-  ( ( X e. J /\ ( X \ o ) C_ X /\ ( X \ o ) =/= (/) ) -> { x e. ~P X | ( X \ o ) C_ x } e. ( Fil ` X ) )
102 33 92 100 101 syl3anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> { x e. ~P X | ( X \ o ) C_ x } e. ( Fil ` X ) )
103 filfbas 
 |-  ( { x e. ~P X | ( X \ o ) C_ x } e. ( Fil ` X ) -> { x e. ~P X | ( X \ o ) C_ x } e. ( fBas ` X ) )
104 102 103 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> { x e. ~P X | ( X \ o ) C_ x } e. ( fBas ` X ) )
105 fbunfip 
 |-  ( ( F e. ( fBas ` X ) /\ { x e. ~P X | ( X \ o ) C_ x } e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) <-> A. y e. F A. z e. { x e. ~P X | ( X \ o ) C_ x } ( y i^i z ) =/= (/) ) )
106 91 104 105 syl2anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( -. (/) e. ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) <-> A. y e. F A. z e. { x e. ~P X | ( X \ o ) C_ x } ( y i^i z ) =/= (/) ) )
107 89 106 mpbird 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> -. (/) e. ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) )
108 fsubbas 
 |-  ( X e. F -> ( ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) e. ( fBas ` X ) <-> ( ( F u. { x e. ~P X | ( X \ o ) C_ x } ) C_ ~P X /\ ( F u. { x e. ~P X | ( X \ o ) C_ x } ) =/= (/) /\ -. (/) e. ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) )
109 94 108 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) e. ( fBas ` X ) <-> ( ( F u. { x e. ~P X | ( X \ o ) C_ x } ) C_ ~P X /\ ( F u. { x e. ~P X | ( X \ o ) C_ x } ) =/= (/) /\ -. (/) e. ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) )
110 45 56 107 109 mpbir3and 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) e. ( fBas ` X ) )
111 ssfg 
 |-  ( ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) e. ( fBas ` X ) -> ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) C_ ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) )
112 110 111 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) C_ ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) )
113 40 112 sstrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( F u. { x e. ~P X | ( X \ o ) C_ x } ) C_ ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) )
114 113 unssad 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> F C_ ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) )
115 fgcl 
 |-  ( ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) e. ( Fil ` X ) )
116 110 115 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) e. ( Fil ` X ) )
117 sseq2 
 |-  ( g = ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) -> ( F C_ g <-> F C_ ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) )
118 oveq2 
 |-  ( g = ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) -> ( J fClus g ) = ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) )
119 118 eleq2d 
 |-  ( g = ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) -> ( A e. ( J fClus g ) <-> A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) )
120 117 119 imbi12d 
 |-  ( g = ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) -> ( ( F C_ g -> A e. ( J fClus g ) ) <-> ( F C_ ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) -> A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) ) )
121 120 rspcv 
 |-  ( ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) e. ( Fil ` X ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> ( F C_ ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) -> A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) ) )
122 116 121 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> ( F C_ ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) -> A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) ) )
123 114 122 mpid 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) )
124 simpr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) -> A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) )
125 simplrl 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) -> o e. J )
126 simprrl 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> A e. o )
127 126 adantr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) -> A e. o )
128 113 55 sseldd 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( X \ o ) e. ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) )
129 128 adantr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) -> ( X \ o ) e. ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) )
130 fclsopni 
 |-  ( ( A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) /\ ( o e. J /\ A e. o /\ ( X \ o ) e. ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) -> ( o i^i ( X \ o ) ) =/= (/) )
131 124 125 127 129 130 syl13anc 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) /\ A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) ) -> ( o i^i ( X \ o ) ) =/= (/) )
132 131 ex 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( A e. ( J fClus ( X filGen ( fi ` ( F u. { x e. ~P X | ( X \ o ) C_ x } ) ) ) ) -> ( o i^i ( X \ o ) ) =/= (/) ) )
133 123 132 syld 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> ( o i^i ( X \ o ) ) =/= (/) ) )
134 133 necon2bd 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> ( ( o i^i ( X \ o ) ) = (/) -> -. A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) ) )
135 29 134 mpi 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ ( o e. J /\ ( A e. o /\ -. o e. F ) ) ) -> -. A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) )
136 135 anassrs 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ o e. J ) /\ ( A e. o /\ -. o e. F ) ) -> -. A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) )
137 136 expr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ o e. J ) /\ A e. o ) -> ( -. o e. F -> -. A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) ) )
138 137 con4d 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ o e. J ) /\ A e. o ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> o e. F ) )
139 138 ex 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ o e. J ) -> ( A e. o -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> o e. F ) ) )
140 139 com23 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) /\ o e. J ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> ( A e. o -> o e. F ) ) )
141 140 ralrimdva 
 |-  ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> A. o e. J ( A e. o -> o e. F ) ) )
142 simprr 
 |-  ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) -> A e. X )
143 141 142 jctild 
 |-  ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> ( A e. X /\ A. o e. J ( A e. o -> o e. F ) ) ) )
144 simprl 
 |-  ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) -> J e. Top )
145 144 4 sylib 
 |-  ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) -> J e. ( TopOn ` X ) )
146 simpl 
 |-  ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) -> F e. ( Fil ` X ) )
147 flimopn 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. o e. J ( A e. o -> o e. F ) ) ) )
148 145 146 147 syl2anc 
 |-  ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. o e. J ( A e. o -> o e. F ) ) ) )
149 143 148 sylibrd 
 |-  ( ( F e. ( Fil ` X ) /\ ( J e. Top /\ A e. X ) ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> A e. ( J fLim F ) ) )
150 149 ex 
 |-  ( F e. ( Fil ` X ) -> ( ( J e. Top /\ A e. X ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> A e. ( J fLim F ) ) ) )
151 150 com23 
 |-  ( F e. ( Fil ` X ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> ( ( J e. Top /\ A e. X ) -> A e. ( J fLim F ) ) ) )
152 28 151 mpdd 
 |-  ( F e. ( Fil ` X ) -> ( A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) -> A e. ( J fLim F ) ) )
153 15 152 impbid2 
 |-  ( F e. ( Fil ` X ) -> ( A e. ( J fLim F ) <-> A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) ) )