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 ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → G ⁡ A ∈ K fLimf L ⁡ G ∘ F

Proof

Step Hyp Ref Expression
1 simprl ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → A ∈ J fLimf L ⁡ F
2 flfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
3 2 adantr ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
4 1 3 eleqtrd ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → A ∈ J fLim X FilMap F ⁡ L
5 simprr ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → G ∈ J CnP K ⁡ A
6 cnpflfi ⊢ A ∈ J fLim X FilMap F ⁡ L ∧ G ∈ J CnP K ⁡ A → G ⁡ A ∈ K fLimf X FilMap F ⁡ L ⁡ G
7 4 5 6 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → G ⁡ A ∈ K fLimf X FilMap F ⁡ L ⁡ G
8 cnptop2 ⊢ G ∈ J CnP K ⁡ A → K ∈ Top
9 8 ad2antll ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → K ∈ Top
10 toptopon2 ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ ⋃ K
11 9 10 sylib ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ 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 ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → ⋃ K ∈ K
14 simpl1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ 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 ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → X ∈ J
17 simpl2 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ 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 ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → L ∈ fBas ⁡ Y
20 cnpf2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ ⋃ K ∧ G ∈ J CnP K ⁡ A → G : X ⟶ ⋃ K
21 14 11 5 20 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → G : X ⟶ ⋃ K
22 simpl3 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → F : Y ⟶ X
23 fmco ⊢ ⋃ K ∈ K ∧ X ∈ J ∧ L ∈ fBas ⁡ Y ∧ G : X ⟶ ⋃ K ∧ F : Y ⟶ X → ⋃ K FilMap G ∘ F ⁡ L = ⋃ K FilMap G ⁡ X FilMap F ⁡ L
24 13 16 19 21 22 23 syl32anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → ⋃ K FilMap G ∘ F ⁡ L = ⋃ K FilMap G ⁡ X FilMap F ⁡ L
25 24 oveq2d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → K fLim ⋃ K FilMap G ∘ F ⁡ L = K fLim ⋃ K FilMap G ⁡ X FilMap F ⁡ 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 ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → G ∘ F : Y ⟶ ⋃ K
28 flfval ⊢ K ∈ TopOn ⁡ ⋃ K ∧ L ∈ Fil ⁡ Y ∧ G ∘ F : Y ⟶ ⋃ K → K fLimf L ⁡ G ∘ F = K fLim ⋃ K FilMap G ∘ F ⁡ L
29 11 17 27 28 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → K fLimf L ⁡ G ∘ F = K fLim ⋃ K FilMap G ∘ F ⁡ L
30 fmfil ⊢ X ∈ J ∧ L ∈ fBas ⁡ Y ∧ F : Y ⟶ X → X FilMap F ⁡ L ∈ Fil ⁡ X
31 16 19 22 30 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → X FilMap F ⁡ L ∈ Fil ⁡ X
32 flfval ⊢ K ∈ TopOn ⁡ ⋃ K ∧ X FilMap F ⁡ L ∈ Fil ⁡ X ∧ G : X ⟶ ⋃ K → K fLimf X FilMap F ⁡ L ⁡ G = K fLim ⋃ K FilMap G ⁡ X FilMap F ⁡ L
33 11 31 21 32 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → K fLimf X FilMap F ⁡ L ⁡ G = K fLim ⋃ K FilMap G ⁡ X FilMap F ⁡ L
34 25 29 33 3eqtr4d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → K fLimf L ⁡ G ∘ F = K fLimf X FilMap F ⁡ L ⁡ G
35 7 34 eleqtrrd ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ G ∈ J CnP K ⁡ A → G ⁡ A ∈ K fLimf L ⁡ G ∘ F