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