Metamath Proof Explorer

Theorem flfcnp

Description: A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Assertion flfcnp 
|- ( ( ( 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 ) ) )

Proof

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 ) ) )