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

Definition df-cnp 16790
 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 16787 . 2
2 vj . . 3
3 vk . . 3
4 ctop 16463 . . 3
5 vx . . . 4
62cv 1618 . . . . 5
76cuni 3727 . . . 4
85cv 1618 . . . . . . . . 9
9 vf . . . . . . . . . 10
109cv 1618 . . . . . . . . 9
118, 10cfv 4592 . . . . . . . 8
12 vy . . . . . . . . 9
1312cv 1618 . . . . . . . 8
1411, 13wcel 1621 . . . . . . 7
15 vg . . . . . . . . . 10
165, 15wel 1622 . . . . . . . . 9
1715cv 1618 . . . . . . . . . . 11
1810, 17cima 4583 . . . . . . . . . 10
1918, 13wss 3078 . . . . . . . . 9
2016, 19wa 360 . . . . . . . 8
2120, 15, 6wrex 2510 . . . . . . 7
2214, 21wi 6 . . . . . 6
233cv 1618 . . . . . 6
2422, 12, 23wral 2509 . . . . 5
2523cuni 3727 . . . . . 6
26 cmap 6658 . . . . . 6
2725, 7, 26co 5710 . . . . 5
2824, 9, 27crab 2512 . . . 4
295, 7, 28cmpt 3974 . . 3
302, 3, 4, 4, 29cmpt2 5712 . 2
311, 30wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  cnpfval  16796  iscnp2  16801
 Copyright terms: Public domain W3C validator