# 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 e. ( J Cn K ) -> F e. ( ( kGen ` J ) Cn ( kGen ` K ) ) )`

### Proof

Step Hyp Ref Expression
1 cntop1
` |-  ( F e. ( J Cn K ) -> J e. Top )`
2 toptopon2
` |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )`
3 1 2 sylib
` |-  ( F e. ( J Cn K ) -> J e. ( TopOn ` U. J ) )`
4 kgentopon
` |-  ( J e. ( TopOn ` U. J ) -> ( kGen ` J ) e. ( TopOn ` U. J ) )`
5 3 4 syl
` |-  ( F e. ( J Cn K ) -> ( kGen ` J ) e. ( TopOn ` U. J ) )`
6 kgenss
` |-  ( J e. Top -> J C_ ( kGen ` J ) )`
7 1 6 syl
` |-  ( F e. ( J Cn K ) -> J C_ ( kGen ` J ) )`
8 eqid
` |-  U. J = U. J`
9 8 cnss1
` |-  ( ( ( kGen ` J ) e. ( TopOn ` U. J ) /\ J C_ ( kGen ` J ) ) -> ( J Cn K ) C_ ( ( kGen ` J ) Cn K ) )`
10 5 7 9 syl2anc
` |-  ( F e. ( J Cn K ) -> ( J Cn K ) C_ ( ( kGen ` J ) Cn K ) )`
11 kgenf
` |-  kGen : Top --> Top`
12 ffn
` |-  ( kGen : Top --> Top -> kGen Fn Top )`
13 11 12 ax-mp
` |-  kGen Fn Top`
14 fnfvelrn
` |-  ( ( kGen Fn Top /\ J e. Top ) -> ( kGen ` J ) e. ran kGen )`
15 13 1 14 sylancr
` |-  ( F e. ( J Cn K ) -> ( kGen ` J ) e. ran kGen )`
16 cntop2
` |-  ( F e. ( J Cn K ) -> K e. Top )`
17 kgencn3
` |-  ( ( ( kGen ` J ) e. ran kGen /\ K e. Top ) -> ( ( kGen ` J ) Cn K ) = ( ( kGen ` J ) Cn ( kGen ` K ) ) )`
18 15 16 17 syl2anc
` |-  ( F e. ( J Cn K ) -> ( ( kGen ` J ) Cn K ) = ( ( kGen ` J ) Cn ( kGen ` K ) ) )`
19 10 18 sseqtrd
` |-  ( F e. ( J Cn K ) -> ( J Cn K ) C_ ( ( kGen ` J ) Cn ( kGen ` K ) ) )`
20 id
` |-  ( F e. ( J Cn K ) -> F e. ( J Cn K ) )`
21 19 20 sseldd
` |-  ( F e. ( J Cn K ) -> F e. ( ( kGen ` J ) Cn ( kGen ` K ) ) )`