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 FJCnKF𝑘GenJCn𝑘GenK

Proof

Step Hyp Ref Expression
1 cntop1 FJCnKJTop
2 toptopon2 JTopJTopOnJ
3 1 2 sylib FJCnKJTopOnJ
4 kgentopon JTopOnJ𝑘GenJTopOnJ
5 3 4 syl FJCnK𝑘GenJTopOnJ
6 kgenss JTopJ𝑘GenJ
7 1 6 syl FJCnKJ𝑘GenJ
8 eqid J=J
9 8 cnss1 𝑘GenJTopOnJJ𝑘GenJJCnK𝑘GenJCnK
10 5 7 9 syl2anc FJCnKJCnK𝑘GenJCnK
11 kgenf 𝑘Gen:TopTop
12 ffn 𝑘Gen:TopTop𝑘GenFnTop
13 11 12 ax-mp 𝑘GenFnTop
14 fnfvelrn 𝑘GenFnTopJTop𝑘GenJran𝑘Gen
15 13 1 14 sylancr FJCnK𝑘GenJran𝑘Gen
16 cntop2 FJCnKKTop
17 kgencn3 𝑘GenJran𝑘GenKTop𝑘GenJCnK=𝑘GenJCn𝑘GenK
18 15 16 17 syl2anc FJCnK𝑘GenJCnK=𝑘GenJCn𝑘GenK
19 10 18 sseqtrd FJCnKJCnK𝑘GenJCn𝑘GenK
20 id FJCnKFJCnK
21 19 20 sseldd FJCnKF𝑘GenJCn𝑘GenK