| Step |
Hyp |
Ref |
Expression |
| 1 |
|
limcflf.f |
|- ( ph -> F : A --> CC ) |
| 2 |
|
limcflf.a |
|- ( ph -> A C_ CC ) |
| 3 |
|
limcflf.b |
|- ( ph -> B e. ( ( limPt ` K ) ` A ) ) |
| 4 |
|
limcflf.k |
|- K = ( TopOpen ` CCfld ) |
| 5 |
|
limcflf.c |
|- C = ( A \ { B } ) |
| 6 |
|
limcflf.l |
|- L = ( ( ( nei ` K ) ` { B } ) |`t C ) |
| 7 |
4
|
cnfldtop |
|- K e. Top |
| 8 |
4
|
cnfldtopon |
|- K e. ( TopOn ` CC ) |
| 9 |
8
|
toponunii |
|- CC = U. K |
| 10 |
9
|
islp |
|- ( ( K e. Top /\ A C_ CC ) -> ( B e. ( ( limPt ` K ) ` A ) <-> B e. ( ( cls ` K ) ` ( A \ { B } ) ) ) ) |
| 11 |
7 2 10
|
sylancr |
|- ( ph -> ( B e. ( ( limPt ` K ) ` A ) <-> B e. ( ( cls ` K ) ` ( A \ { B } ) ) ) ) |
| 12 |
3 11
|
mpbid |
|- ( ph -> B e. ( ( cls ` K ) ` ( A \ { B } ) ) ) |
| 13 |
5
|
fveq2i |
|- ( ( cls ` K ) ` C ) = ( ( cls ` K ) ` ( A \ { B } ) ) |
| 14 |
12 13
|
eleqtrrdi |
|- ( ph -> B e. ( ( cls ` K ) ` C ) ) |
| 15 |
|
difss |
|- ( A \ { B } ) C_ A |
| 16 |
5 15
|
eqsstri |
|- C C_ A |
| 17 |
16 2
|
sstrid |
|- ( ph -> C C_ CC ) |
| 18 |
9
|
lpss |
|- ( ( K e. Top /\ A C_ CC ) -> ( ( limPt ` K ) ` A ) C_ CC ) |
| 19 |
7 2 18
|
sylancr |
|- ( ph -> ( ( limPt ` K ) ` A ) C_ CC ) |
| 20 |
19 3
|
sseldd |
|- ( ph -> B e. CC ) |
| 21 |
|
trnei |
|- ( ( K e. ( TopOn ` CC ) /\ C C_ CC /\ B e. CC ) -> ( B e. ( ( cls ` K ) ` C ) <-> ( ( ( nei ` K ) ` { B } ) |`t C ) e. ( Fil ` C ) ) ) |
| 22 |
8 17 20 21
|
mp3an2i |
|- ( ph -> ( B e. ( ( cls ` K ) ` C ) <-> ( ( ( nei ` K ) ` { B } ) |`t C ) e. ( Fil ` C ) ) ) |
| 23 |
14 22
|
mpbid |
|- ( ph -> ( ( ( nei ` K ) ` { B } ) |`t C ) e. ( Fil ` C ) ) |
| 24 |
6 23
|
eqeltrid |
|- ( ph -> L e. ( Fil ` C ) ) |