# Metamath Proof Explorer

## Theorem kgen2cn

Description: A continuous function is also continuous with the domain and codomain replaced by their compact generator topologies. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgen2cn ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {F}\in \left(\mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cntop1 ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {J}\in \mathrm{Top}$
2 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
3 1 2 sylib ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
4 kgentopon ${⊢}{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left(\bigcup {J}\right)$
5 3 4 syl ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left(\bigcup {J}\right)$
6 kgenss ${⊢}{J}\in \mathrm{Top}\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
7 1 6 syl ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
8 eqid ${⊢}\bigcup {J}=\bigcup {J}$
9 8 cnss1 ${⊢}\left(\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left(\bigcup {J}\right)\wedge {J}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\to {J}\mathrm{Cn}{K}\subseteq \mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}{K}$
10 5 7 9 syl2anc ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {J}\mathrm{Cn}{K}\subseteq \mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}{K}$
11 kgenf ${⊢}\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}$
12 ffn ${⊢}\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}\to \mathrm{𝑘Gen}Fn\mathrm{Top}$
13 11 12 ax-mp ${⊢}\mathrm{𝑘Gen}Fn\mathrm{Top}$
14 fnfvelrn ${⊢}\left(\mathrm{𝑘Gen}Fn\mathrm{Top}\wedge {J}\in \mathrm{Top}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{ran}\mathrm{𝑘Gen}$
15 13 1 14 sylancr ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{ran}\mathrm{𝑘Gen}$
16 cntop2 ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {K}\in \mathrm{Top}$
17 kgencn3 ${⊢}\left(\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{ran}\mathrm{𝑘Gen}\wedge {K}\in \mathrm{Top}\right)\to \mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}{K}=\mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)$
18 15 16 17 syl2anc ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to \mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}{K}=\mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)$
19 10 18 sseqtrd ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {J}\mathrm{Cn}{K}\subseteq \mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)$
20 id ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
21 19 20 sseldd ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {F}\in \left(\mathrm{𝑘Gen}\left({J}\right)\mathrm{Cn}\mathrm{𝑘Gen}\left({K}\right)\right)$