This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 ∈ ( ( 𝑘Gen ‘ 𝐽 ) Cn ( 𝑘Gen ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
2 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
3 1 2 sylib ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
4 kgentopon ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ( TopOn ‘ ∪ 𝐽 ) )
5 3 4 syl ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ( TopOn ‘ ∪ 𝐽 ) )
6 kgenss ⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
7 1 6 syl ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
8 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
9 8 cnss1 ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝐽 Cn 𝐾 ) ⊆ ( ( 𝑘Gen ‘ 𝐽 ) Cn 𝐾 ) )
10 5 7 9 syl2anc ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐽 Cn 𝐾 ) ⊆ ( ( 𝑘Gen ‘ 𝐽 ) Cn 𝐾 ) )
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 ∧ 𝐽 ∈ Top ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen )
15 13 1 14 sylancr ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen )
16 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
17 kgencn3 ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → ( ( 𝑘Gen ‘ 𝐽 ) Cn 𝐾 ) = ( ( 𝑘Gen ‘ 𝐽 ) Cn ( 𝑘Gen ‘ 𝐾 ) ) )
18 15 16 17 syl2anc ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( ( 𝑘Gen ‘ 𝐽 ) Cn 𝐾 ) = ( ( 𝑘Gen ‘ 𝐽 ) Cn ( 𝑘Gen ‘ 𝐾 ) ) )
19 10 18 sseqtrd ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐽 Cn 𝐾 ) ⊆ ( ( 𝑘Gen ‘ 𝐽 ) Cn ( 𝑘Gen ‘ 𝐾 ) ) )
20 id ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
21 19 20 sseldd ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 ∈ ( ( 𝑘Gen ‘ 𝐽 ) Cn ( 𝑘Gen ‘ 𝐾 ) ) )