Metamath Proof Explorer

Theorem flfcnp

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

Ref Expression
Assertion flfcnp ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→G⁡A∈KfLimfL⁡G∘F

Proof

Step Hyp Ref Expression
1 simprl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→A∈JfLimfL⁡F
2 flfval ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→JfLimfL⁡F=JfLimXFilMapF⁡L
3 2 adantr ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→JfLimfL⁡F=JfLimXFilMapF⁡L
4 1 3 eleqtrd ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→A∈JfLimXFilMapF⁡L
5 simprr ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→G∈JCnPK⁡A
6 cnpflfi ⊢A∈JfLimXFilMapF⁡L∧G∈JCnPK⁡A→G⁡A∈KfLimfXFilMapF⁡L⁡G
7 4 5 6 syl2anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→G⁡A∈KfLimfXFilMapF⁡L⁡G
8 cnptop2 ⊢G∈JCnPK⁡A→K∈Top
9 8 ad2antll ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→K∈Top
10 toptopon2 ⊢K∈Top↔K∈TopOn⁡⋃K
11 9 10 sylib ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→K∈TopOn⁡⋃K
12 toponmax ⊢K∈TopOn⁡⋃K→⋃K∈K
13 11 12 syl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→⋃K∈K
14 simpl1 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→J∈TopOn⁡X
15 toponmax ⊢J∈TopOn⁡X→X∈J
16 14 15 syl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→X∈J
17 simpl2 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→L∈Fil⁡Y
18 filfbas ⊢L∈Fil⁡Y→L∈fBas⁡Y
19 17 18 syl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→L∈fBas⁡Y
20 cnpf2 ⊢J∈TopOn⁡X∧K∈TopOn⁡⋃K∧G∈JCnPK⁡A→G:X⟶⋃K
21 14 11 5 20 syl3anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→G:X⟶⋃K
22 simpl3 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→F:Y⟶X
23 fmco ⊢⋃K∈K∧X∈J∧L∈fBas⁡Y∧G:X⟶⋃K∧F:Y⟶X→⋃KFilMapG∘F⁡L=⋃KFilMapG⁡XFilMapF⁡L
24 13 16 19 21 22 23 syl32anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→⋃KFilMapG∘F⁡L=⋃KFilMapG⁡XFilMapF⁡L
25 24 oveq2d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→KfLim⋃KFilMapG∘F⁡L=KfLim⋃KFilMapG⁡XFilMapF⁡L
26 fco ⊢G:X⟶⋃K∧F:Y⟶X→G∘F:Y⟶⋃K
27 21 22 26 syl2anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→G∘F:Y⟶⋃K
28 flfval ⊢K∈TopOn⁡⋃K∧L∈Fil⁡Y∧G∘F:Y⟶⋃K→KfLimfL⁡G∘F=KfLim⋃KFilMapG∘F⁡L
29 11 17 27 28 syl3anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→KfLimfL⁡G∘F=KfLim⋃KFilMapG∘F⁡L
30 fmfil ⊢X∈J∧L∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡L∈Fil⁡X
31 16 19 22 30 syl3anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→XFilMapF⁡L∈Fil⁡X
32 flfval ⊢K∈TopOn⁡⋃K∧XFilMapF⁡L∈Fil⁡X∧G:X⟶⋃K→KfLimfXFilMapF⁡L⁡G=KfLim⋃KFilMapG⁡XFilMapF⁡L
33 11 31 21 32 syl3anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→KfLimfXFilMapF⁡L⁡G=KfLim⋃KFilMapG⁡XFilMapF⁡L
34 25 29 33 3eqtr4d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→KfLimfL⁡G∘F=KfLimfXFilMapF⁡L⁡G
35 7 34 eleqtrrd ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧A∈JfLimfL⁡F∧G∈JCnPK⁡A→G⁡A∈KfLimfL⁡G∘F