Step |
Hyp |
Ref |
Expression |
1 |
|
simprl |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> A e. ( ( J fLimf L ) ` F ) ) |
2 |
|
flfval |
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) ) |
3 |
2
|
adantr |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) ) |
4 |
1 3
|
eleqtrd |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> A e. ( J fLim ( ( X FilMap F ) ` L ) ) ) |
5 |
|
simprr |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> G e. ( ( J CnP K ) ` A ) ) |
6 |
|
cnpflfi |
|- ( ( A e. ( J fLim ( ( X FilMap F ) ` L ) ) /\ G e. ( ( J CnP K ) ` A ) ) -> ( G ` A ) e. ( ( K fLimf ( ( X FilMap F ) ` L ) ) ` G ) ) |
7 |
4 5 6
|
syl2anc |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( G ` A ) e. ( ( K fLimf ( ( X FilMap F ) ` L ) ) ` G ) ) |
8 |
|
cnptop2 |
|- ( G e. ( ( J CnP K ) ` A ) -> K e. Top ) |
9 |
8
|
ad2antll |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> K e. Top ) |
10 |
|
toptopon2 |
|- ( K e. Top <-> K e. ( TopOn ` U. K ) ) |
11 |
9 10
|
sylib |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> K e. ( TopOn ` U. K ) ) |
12 |
|
toponmax |
|- ( K e. ( TopOn ` U. K ) -> U. K e. K ) |
13 |
11 12
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> U. K e. K ) |
14 |
|
simpl1 |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> J e. ( TopOn ` X ) ) |
15 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
16 |
14 15
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> X e. J ) |
17 |
|
simpl2 |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> L e. ( Fil ` Y ) ) |
18 |
|
filfbas |
|- ( L e. ( Fil ` Y ) -> L e. ( fBas ` Y ) ) |
19 |
17 18
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> L e. ( fBas ` Y ) ) |
20 |
|
cnpf2 |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) /\ G e. ( ( J CnP K ) ` A ) ) -> G : X --> U. K ) |
21 |
14 11 5 20
|
syl3anc |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> G : X --> U. K ) |
22 |
|
simpl3 |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> F : Y --> X ) |
23 |
|
fmco |
|- ( ( ( U. K e. K /\ X e. J /\ L e. ( fBas ` Y ) ) /\ ( G : X --> U. K /\ F : Y --> X ) ) -> ( ( U. K FilMap ( G o. F ) ) ` L ) = ( ( U. K FilMap G ) ` ( ( X FilMap F ) ` L ) ) ) |
24 |
13 16 19 21 22 23
|
syl32anc |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( ( U. K FilMap ( G o. F ) ) ` L ) = ( ( U. K FilMap G ) ` ( ( X FilMap F ) ` L ) ) ) |
25 |
24
|
oveq2d |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( K fLim ( ( U. K FilMap ( G o. F ) ) ` L ) ) = ( K fLim ( ( U. K FilMap G ) ` ( ( X FilMap F ) ` L ) ) ) ) |
26 |
|
fco |
|- ( ( G : X --> U. K /\ F : Y --> X ) -> ( G o. F ) : Y --> U. K ) |
27 |
21 22 26
|
syl2anc |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( G o. F ) : Y --> U. K ) |
28 |
|
flfval |
|- ( ( K e. ( TopOn ` U. K ) /\ L e. ( Fil ` Y ) /\ ( G o. F ) : Y --> U. K ) -> ( ( K fLimf L ) ` ( G o. F ) ) = ( K fLim ( ( U. K FilMap ( G o. F ) ) ` L ) ) ) |
29 |
11 17 27 28
|
syl3anc |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( ( K fLimf L ) ` ( G o. F ) ) = ( K fLim ( ( U. K FilMap ( G o. F ) ) ` L ) ) ) |
30 |
|
fmfil |
|- ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) ) |
31 |
16 19 22 30
|
syl3anc |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) ) |
32 |
|
flfval |
|- ( ( K e. ( TopOn ` U. K ) /\ ( ( X FilMap F ) ` L ) e. ( Fil ` X ) /\ G : X --> U. K ) -> ( ( K fLimf ( ( X FilMap F ) ` L ) ) ` G ) = ( K fLim ( ( U. K FilMap G ) ` ( ( X FilMap F ) ` L ) ) ) ) |
33 |
11 31 21 32
|
syl3anc |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( ( K fLimf ( ( X FilMap F ) ` L ) ) ` G ) = ( K fLim ( ( U. K FilMap G ) ` ( ( X FilMap F ) ` L ) ) ) ) |
34 |
25 29 33
|
3eqtr4d |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( ( K fLimf L ) ` ( G o. F ) ) = ( ( K fLimf ( ( X FilMap F ) ` L ) ) ` G ) ) |
35 |
7 34
|
eleqtrrd |
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( G ` A ) e. ( ( K fLimf L ) ` ( G o. F ) ) ) |