Step |
Hyp |
Ref |
Expression |
1 |
|
flfval |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) ) |
2 |
1
|
eleq2d |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> A e. ( J fLim ( ( X FilMap F ) ` L ) ) ) ) |
3 |
|
simp1 |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> J e. ( TopOn ` X ) ) |
4 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
5 |
4
|
3ad2ant1 |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> X e. J ) |
6 |
|
filfbas |
|- ( L e. ( Fil ` Y ) -> L e. ( fBas ` Y ) ) |
7 |
6
|
3ad2ant2 |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> L e. ( fBas ` Y ) ) |
8 |
|
simp3 |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> F : Y --> X ) |
9 |
|
fmfil |
|- ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) ) |
10 |
5 7 8 9
|
syl3anc |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) ) |
11 |
|
elflim |
|- ( ( J e. ( TopOn ` X ) /\ ( ( X FilMap F ) ` L ) e. ( Fil ` X ) ) -> ( A e. ( J fLim ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) ) ) ) |
12 |
3 10 11
|
syl2anc |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( J fLim ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) ) ) ) |
13 |
|
dfss3 |
|- ( ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) <-> A. n e. ( ( nei ` J ) ` { A } ) n e. ( ( X FilMap F ) ` L ) ) |
14 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
15 |
14
|
3ad2ant1 |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> J e. Top ) |
16 |
|
eqid |
|- U. J = U. J |
17 |
16
|
neii1 |
|- ( ( J e. Top /\ n e. ( ( nei ` J ) ` { A } ) ) -> n C_ U. J ) |
18 |
15 17
|
sylan |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> n C_ U. J ) |
19 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
20 |
19
|
3ad2ant1 |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> X = U. J ) |
21 |
20
|
adantr |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> X = U. J ) |
22 |
18 21
|
sseqtrrd |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> n C_ X ) |
23 |
|
elfm |
|- ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( n e. ( ( X FilMap F ) ` L ) <-> ( n C_ X /\ E. s e. L ( F " s ) C_ n ) ) ) |
24 |
5 7 8 23
|
syl3anc |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( n e. ( ( X FilMap F ) ` L ) <-> ( n C_ X /\ E. s e. L ( F " s ) C_ n ) ) ) |
25 |
24
|
baibd |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n C_ X ) -> ( n e. ( ( X FilMap F ) ` L ) <-> E. s e. L ( F " s ) C_ n ) ) |
26 |
22 25
|
syldan |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( n e. ( ( X FilMap F ) ` L ) <-> E. s e. L ( F " s ) C_ n ) ) |
27 |
26
|
ralbidva |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A. n e. ( ( nei ` J ) ` { A } ) n e. ( ( X FilMap F ) ` L ) <-> A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) |
28 |
13 27
|
syl5bb |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) <-> A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) |
29 |
28
|
anbi2d |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) ) |
30 |
2 12 29
|
3bitrd |
|- ( ( 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 ) ) ) |