Step |
Hyp |
Ref |
Expression |
1 |
|
flftg.l |
|- J = ( topGen ` B ) |
2 |
|
isflf |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. u e. J ( A e. u -> E. s e. L ( F " s ) C_ u ) ) ) ) |
3 |
1
|
raleqi |
|- ( A. u e. J ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) ) |
4 |
|
simpl1 |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> J e. ( TopOn ` X ) ) |
5 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
6 |
4 5
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> J e. Top ) |
7 |
1 6
|
eqeltrrid |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( topGen ` B ) e. Top ) |
8 |
|
tgclb |
|- ( B e. TopBases <-> ( topGen ` B ) e. Top ) |
9 |
7 8
|
sylibr |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> B e. TopBases ) |
10 |
|
bastg |
|- ( B e. TopBases -> B C_ ( topGen ` B ) ) |
11 |
|
eleq2w |
|- ( u = o -> ( A e. u <-> A e. o ) ) |
12 |
|
sseq2 |
|- ( u = o -> ( ( F " s ) C_ u <-> ( F " s ) C_ o ) ) |
13 |
12
|
rexbidv |
|- ( u = o -> ( E. s e. L ( F " s ) C_ u <-> E. s e. L ( F " s ) C_ o ) ) |
14 |
11 13
|
imbi12d |
|- ( u = o -> ( ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) |
15 |
14
|
cbvralvw |
|- ( A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> A. o e. ( topGen ` B ) ( A e. o -> E. s e. L ( F " s ) C_ o ) ) |
16 |
|
ssralv |
|- ( B C_ ( topGen ` B ) -> ( A. o e. ( topGen ` B ) ( A e. o -> E. s e. L ( F " s ) C_ o ) -> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) |
17 |
15 16
|
syl5bi |
|- ( B C_ ( topGen ` B ) -> ( A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) -> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) |
18 |
9 10 17
|
3syl |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) -> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) |
19 |
|
tg2 |
|- ( ( u e. ( topGen ` B ) /\ A e. u ) -> E. o e. B ( A e. o /\ o C_ u ) ) |
20 |
|
r19.29 |
|- ( ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ E. o e. B ( A e. o /\ o C_ u ) ) -> E. o e. B ( ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ ( A e. o /\ o C_ u ) ) ) |
21 |
|
simpl |
|- ( ( A e. o /\ o C_ u ) -> A e. o ) |
22 |
|
simpr |
|- ( ( A e. o /\ o C_ u ) -> o C_ u ) |
23 |
|
sstr2 |
|- ( ( F " s ) C_ o -> ( o C_ u -> ( F " s ) C_ u ) ) |
24 |
22 23
|
syl5com |
|- ( ( A e. o /\ o C_ u ) -> ( ( F " s ) C_ o -> ( F " s ) C_ u ) ) |
25 |
24
|
reximdv |
|- ( ( A e. o /\ o C_ u ) -> ( E. s e. L ( F " s ) C_ o -> E. s e. L ( F " s ) C_ u ) ) |
26 |
21 25
|
embantd |
|- ( ( A e. o /\ o C_ u ) -> ( ( A e. o -> E. s e. L ( F " s ) C_ o ) -> E. s e. L ( F " s ) C_ u ) ) |
27 |
26
|
impcom |
|- ( ( ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ ( A e. o /\ o C_ u ) ) -> E. s e. L ( F " s ) C_ u ) |
28 |
27
|
rexlimivw |
|- ( E. o e. B ( ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ ( A e. o /\ o C_ u ) ) -> E. s e. L ( F " s ) C_ u ) |
29 |
20 28
|
syl |
|- ( ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ E. o e. B ( A e. o /\ o C_ u ) ) -> E. s e. L ( F " s ) C_ u ) |
30 |
29
|
ex |
|- ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) -> ( E. o e. B ( A e. o /\ o C_ u ) -> E. s e. L ( F " s ) C_ u ) ) |
31 |
19 30
|
syl5 |
|- ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) -> ( ( u e. ( topGen ` B ) /\ A e. u ) -> E. s e. L ( F " s ) C_ u ) ) |
32 |
31
|
expdimp |
|- ( ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ u e. ( topGen ` B ) ) -> ( A e. u -> E. s e. L ( F " s ) C_ u ) ) |
33 |
32
|
ralrimiva |
|- ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) -> A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) ) |
34 |
18 33
|
impbid1 |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) |
35 |
3 34
|
syl5bb |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. u e. J ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) |
36 |
35
|
pm5.32da |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( A e. X /\ A. u e. J ( A e. u -> E. s e. L ( F " s ) C_ u ) ) <-> ( A e. X /\ A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) ) |
37 |
2 36
|
bitrd |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) ) |