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 ‘ 𝐾 ) ) )