This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ) ) ) ) |
| 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 | dfss2 | |- ( 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 | biimtrrid | |- ( ( ( ( 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 ) ) ) ) |