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