Metamath Proof Explorer

Theorem flfcnp

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

Ref Expression
Assertion flfcnp ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐺 ∘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) )
2 flfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
3 2 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
4 1 3 eleqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐴 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
5 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) )
6 cnpflfi ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ‘ 𝐺 ) )
7 4 5 6 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ‘ 𝐺 ) )
8 cnptop2 ⊢ ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → 𝐾 ∈ Top )
9 8 ad2antll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐾 ∈ Top )
10 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
11 9 10 sylib ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
12 toponmax ⊢ ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) → ∪ 𝐾 ∈ 𝐾 )
13 11 12 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ∪ 𝐾 ∈ 𝐾 )
14 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
16 14 15 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝐽 )
17 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
18 filfbas ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
19 17 18 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
20 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐺 : 𝑋 ⟶ ∪ 𝐾 )
21 14 11 5 20 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐺 : 𝑋 ⟶ ∪ 𝐾 )
22 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → 𝐹 : 𝑌 ⟶ 𝑋 )
23 fmco ⊢ ( ( ( ∪ 𝐾 ∈ 𝐾 ∧ 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( 𝐺 : 𝑋 ⟶ ∪ 𝐾 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ) → ( ( ∪ 𝐾 FilMap ( 𝐺 ∘ 𝐹 ) ) ‘ 𝐿 ) = ( ( ∪ 𝐾 FilMap 𝐺 ) ‘ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
24 13 16 19 21 22 23 syl32anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( ( ∪ 𝐾 FilMap ( 𝐺 ∘ 𝐹 ) ) ‘ 𝐿 ) = ( ( ∪ 𝐾 FilMap 𝐺 ) ‘ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
25 24 oveq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( 𝐾 fLim ( ( ∪ 𝐾 FilMap ( 𝐺 ∘ 𝐹 ) ) ‘ 𝐿 ) ) = ( 𝐾 fLim ( ( ∪ 𝐾 FilMap 𝐺 ) ‘ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) )
26 fco ⊢ ( ( 𝐺 : 𝑋 ⟶ ∪ 𝐾 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐺 ∘ 𝐹 ) : 𝑌 ⟶ ∪ 𝐾 )
27 21 22 26 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( 𝐺 ∘ 𝐹 ) : 𝑌 ⟶ ∪ 𝐾 )
28 flfval ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐺 ∘ 𝐹 ) : 𝑌 ⟶ ∪ 𝐾 ) → ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐺 ∘ 𝐹 ) ) = ( 𝐾 fLim ( ( ∪ 𝐾 FilMap ( 𝐺 ∘ 𝐹 ) ) ‘ 𝐿 ) ) )
29 11 17 27 28 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐺 ∘ 𝐹 ) ) = ( 𝐾 fLim ( ( ∪ 𝐾 FilMap ( 𝐺 ∘ 𝐹 ) ) ‘ 𝐿 ) ) )
30 fmfil ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
31 16 19 22 30 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
32 flfval ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 : 𝑋 ⟶ ∪ 𝐾 ) → ( ( 𝐾 fLimf ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ‘ 𝐺 ) = ( 𝐾 fLim ( ( ∪ 𝐾 FilMap 𝐺 ) ‘ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) )
33 11 31 21 32 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( ( 𝐾 fLimf ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ‘ 𝐺 ) = ( 𝐾 fLim ( ( ∪ 𝐾 FilMap 𝐺 ) ‘ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) )
34 25 29 33 3eqtr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐺 ∘ 𝐹 ) ) = ( ( 𝐾 fLimf ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ‘ 𝐺 ) )
35 7 34 eleqtrrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐺 ∘ 𝐹 ) ) )