Step |
Hyp |
Ref |
Expression |
1 |
|
flfneii.x |
|- X = U. J |
2 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` X ) ) |
3 |
|
flfnei |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) ) |
4 |
2 3
|
syl3an1b |
|- ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) ) |
5 |
4
|
simplbda |
|- ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) ) -> A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) |
6 |
5
|
3adant3 |
|- ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) |
7 |
|
sseq2 |
|- ( n = N -> ( ( F " s ) C_ n <-> ( F " s ) C_ N ) ) |
8 |
7
|
rexbidv |
|- ( n = N -> ( E. s e. L ( F " s ) C_ n <-> E. s e. L ( F " s ) C_ N ) ) |
9 |
8
|
rspcv |
|- ( N e. ( ( nei ` J ) ` { A } ) -> ( A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n -> E. s e. L ( F " s ) C_ N ) ) |
10 |
9
|
3ad2ant3 |
|- ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> ( A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n -> E. s e. L ( F " s ) C_ N ) ) |
11 |
6 10
|
mpd |
|- ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> E. s e. L ( F " s ) C_ N ) |