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 ∈ J Cn K → F ∈ 𝑘Gen ⁡ J Cn 𝑘Gen ⁡ K

Proof

Step Hyp Ref Expression
1 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
2 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
3 1 2 sylib ⊢ F ∈ J Cn K → J ∈ TopOn ⁡ ⋃ J
4 kgentopon ⊢ J ∈ TopOn ⁡ ⋃ J → 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J
5 3 4 syl ⊢ F ∈ J Cn K → 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J
6 kgenss ⊢ J ∈ Top → J ⊆ 𝑘Gen ⁡ J
7 1 6 syl ⊢ F ∈ J Cn K → J ⊆ 𝑘Gen ⁡ J
8 eqid ⊢ ⋃ J = ⋃ J
9 8 cnss1 ⊢ 𝑘Gen ⁡ J ∈ TopOn ⁡ ⋃ J ∧ J ⊆ 𝑘Gen ⁡ J → J Cn K ⊆ 𝑘Gen ⁡ J Cn K
10 5 7 9 syl2anc ⊢ F ∈ J Cn K → J Cn K ⊆ 𝑘Gen ⁡ J Cn K
11 kgenf ⊢ 𝑘Gen : Top ⟶ Top
12 ffn ⊢ 𝑘Gen : Top ⟶ Top → 𝑘Gen Fn Top
13 11 12 ax-mp ⊢ 𝑘Gen Fn Top
14 fnfvelrn ⊢ 𝑘Gen Fn Top ∧ J ∈ Top → 𝑘Gen ⁡ J ∈ ran ⁡ 𝑘Gen
15 13 1 14 sylancr ⊢ F ∈ J Cn K → 𝑘Gen ⁡ J ∈ ran ⁡ 𝑘Gen
16 cntop2 ⊢ F ∈ J Cn K → K ∈ Top
17 kgencn3 ⊢ 𝑘Gen ⁡ J ∈ ran ⁡ 𝑘Gen ∧ K ∈ Top → 𝑘Gen ⁡ J Cn K = 𝑘Gen ⁡ J Cn 𝑘Gen ⁡ K
18 15 16 17 syl2anc ⊢ F ∈ J Cn K → 𝑘Gen ⁡ J Cn K = 𝑘Gen ⁡ J Cn 𝑘Gen ⁡ K
19 10 18 sseqtrd ⊢ F ∈ J Cn K → J Cn K ⊆ 𝑘Gen ⁡ J Cn 𝑘Gen ⁡ K
20 id ⊢ F ∈ J Cn K → F ∈ J Cn K
21 19 20 sseldd ⊢ F ∈ J Cn K → F ∈ 𝑘Gen ⁡ J Cn 𝑘Gen ⁡ K