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

Definition df-cnp 17284
 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 17281 . 2
2 vj . . 3
3 vk . . 3
4 ctop 16950 . . 3
5 vx . . . 4
62cv 1651 . . . . 5
76cuni 4007 . . . 4
85cv 1651 . . . . . . . . 9
9 vf . . . . . . . . . 10
109cv 1651 . . . . . . . . 9
118, 10cfv 5446 . . . . . . . 8
12 vy . . . . . . . . 9
1312cv 1651 . . . . . . . 8
1411, 13wcel 1725 . . . . . . 7
15 vg . . . . . . . . . 10
165, 15wel 1726 . . . . . . . . 9
1715cv 1651 . . . . . . . . . . 11
1810, 17cima 4873 . . . . . . . . . 10
1918, 13wss 3312 . . . . . . . . 9
2016, 19wa 359 . . . . . . . 8
2120, 15, 6wrex 2698 . . . . . . 7
2214, 21wi 4 . . . . . 6
233cv 1651 . . . . . 6
2422, 12, 23wral 2697 . . . . 5
2523cuni 4007 . . . . . 6
26 cmap 7010 . . . . . 6
2725, 7, 26co 6073 . . . . 5
2824, 9, 27crab 2701 . . . 4
295, 7, 28cmpt 4258 . . 3
302, 3, 4, 4, 29cmpt2 6075 . 2
311, 30wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  cnpfval  17290  iscnp2  17295
 Copyright terms: Public domain W3C validator