Metamath Proof Explorer


Definition df-cnp

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 CnP=jTop,kTopxjfkj|ykfxygjxgfgy

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnp classCnP
1 vj setvarj
2 ctop classTop
3 vk setvark
4 vx setvarx
5 1 cv setvarj
6 5 cuni classj
7 vf setvarf
8 3 cv setvark
9 8 cuni classk
10 cmap class𝑚
11 9 6 10 co classkj
12 vy setvary
13 7 cv setvarf
14 4 cv setvarx
15 14 13 cfv classfx
16 12 cv setvary
17 15 16 wcel wfffxy
18 vg setvarg
19 18 cv setvarg
20 14 19 wcel wffxg
21 13 19 cima classfg
22 21 16 wss wfffgy
23 20 22 wa wffxgfgy
24 23 18 5 wrex wffgjxgfgy
25 17 24 wi wfffxygjxgfgy
26 25 12 8 wral wffykfxygjxgfgy
27 26 7 11 crab classfkj|ykfxygjxgfgy
28 4 6 27 cmpt classxjfkj|ykfxygjxgfgy
29 1 3 2 2 28 cmpo classjTop,kTopxjfkj|ykfxygjxgfgy
30 0 29 wceq wffCnP=jTop,kTopxjfkj|ykfxygjxgfgy