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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cntop1 | |
|
2 | toptopon2 | |
|
3 | 1 2 | sylib | |
4 | kgentopon | |
|
5 | 3 4 | syl | |
6 | kgenss | |
|
7 | 1 6 | syl | |
8 | eqid | |
|
9 | 8 | cnss1 | |
10 | 5 7 9 | syl2anc | |
11 | kgenf | |
|
12 | ffn | |
|
13 | 11 12 | ax-mp | |
14 | fnfvelrn | |
|
15 | 13 1 14 | sylancr | |
16 | cntop2 | |
|
17 | kgencn3 | |
|
18 | 15 16 17 | syl2anc | |
19 | 10 18 | sseqtrd | |
20 | id | |
|
21 | 19 20 | sseldd | |