Description: Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of Munkres p. 107. (Contributed by NM, 17-Oct-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | df-cnp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccnp | |
|
1 | vj | |
|
2 | ctop | |
|
3 | vk | |
|
4 | vx | |
|
5 | 1 | cv | |
6 | 5 | cuni | |
7 | vf | |
|
8 | 3 | cv | |
9 | 8 | cuni | |
10 | cmap | |
|
11 | 9 6 10 | co | |
12 | vy | |
|
13 | 7 | cv | |
14 | 4 | cv | |
15 | 14 13 | cfv | |
16 | 12 | cv | |
17 | 15 16 | wcel | |
18 | vg | |
|
19 | 18 | cv | |
20 | 14 19 | wcel | |
21 | 13 19 | cima | |
22 | 21 16 | wss | |
23 | 20 22 | wa | |
24 | 23 18 5 | wrex | |
25 | 17 24 | wi | |
26 | 25 12 8 | wral | |
27 | 26 7 11 | crab | |
28 | 4 6 27 | cmpt | |
29 | 1 3 2 2 28 | cmpo | |
30 | 0 29 | wceq | |