Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnp Structured version   Visualization version   Unicode version

Definition df-cnp 20321
 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.)
Assertion
Ref Expression
df-cnp
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-cnp
StepHypRef Expression
1 ccnp 20318 . 2
2 vj . . 3
3 vk . . 3
4 ctop 19994 . . 3
5 vx . . . 4
62cv 1451 . . . . 5
76cuni 4190 . . . 4
85cv 1451 . . . . . . . . 9
9 vf . . . . . . . . . 10
109cv 1451 . . . . . . . . 9
118, 10cfv 5589 . . . . . . . 8
12 vy . . . . . . . . 9
1312cv 1451 . . . . . . . 8
1411, 13wcel 1904 . . . . . . 7
15 vg . . . . . . . . . 10
165, 15wel 1905 . . . . . . . . 9
1715cv 1451 . . . . . . . . . . 11
1810, 17cima 4842 . . . . . . . . . 10
1918, 13wss 3390 . . . . . . . . 9
2016, 19wa 376 . . . . . . . 8
2120, 15, 6wrex 2757 . . . . . . 7
2214, 21wi 4 . . . . . 6
233cv 1451 . . . . . 6
2422, 12, 23wral 2756 . . . . 5
2523cuni 4190 . . . . . 6
26 cmap 7490 . . . . . 6
2725, 7, 26co 6308 . . . . 5
2824, 9, 27crab 2760 . . . 4
295, 7, 28cmpt 4454 . . 3
302, 3, 4, 4, 29cmpt2 6310 . 2
311, 30wceq 1452 1
 Colors of variables: wff setvar class This definition is referenced by:  cnpfval  20327  iscnp2  20332
 Copyright terms: Public domain W3C validator