Description: Continuity of a projection map from the space of continuous functions. (This theorem can be strengthened, to joint continuity in both f and A as a function on ( S ^ko R ) tX R , but not without stronger assumptions on R ; see xkofvcn .) (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | xkopjcn.1 | |
|
Assertion | xkopjcn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xkopjcn.1 | |
|
2 | eqid | |
|
3 | 2 | xkotopon | |
4 | 3 | 3adant3 | |
5 | 1 | topopn | |
6 | 5 | 3ad2ant1 | |
7 | fconst6g | |
|
8 | 7 | 3ad2ant2 | |
9 | pttop | |
|
10 | 6 8 9 | syl2anc | |
11 | eqid | |
|
12 | 1 11 | cnf | |
13 | uniexg | |
|
14 | 13 | 3ad2ant2 | |
15 | 14 6 | elmapd | |
16 | 12 15 | syl5ibr | |
17 | 16 | ssrdv | |
18 | simp2 | |
|
19 | eqid | |
|
20 | 19 11 | ptuniconst | |
21 | 6 18 20 | syl2anc | |
22 | 17 21 | sseqtrd | |
23 | eqid | |
|
24 | 23 | restuni | |
25 | 10 22 24 | syl2anc | |
26 | 25 | fveq2d | |
27 | 4 26 | eleqtrd | |
28 | 1 19 | xkoptsub | |
29 | 28 | 3adant3 | |
30 | eqid | |
|
31 | 30 | cnss1 | |
32 | 27 29 31 | syl2anc | |
33 | 22 | resmptd | |
34 | simp3 | |
|
35 | 23 19 | ptpjcn | |
36 | 6 8 34 35 | syl3anc | |
37 | fvconst2g | |
|
38 | 37 | 3adant1 | |
39 | 38 | oveq2d | |
40 | 36 39 | eleqtrd | |
41 | 23 | cnrest | |
42 | 40 22 41 | syl2anc | |
43 | 33 42 | eqeltrrd | |
44 | 32 43 | sseldd | |