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

Definition df-cnp 16885
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  |-  CnP  =  ( j  e.  Top ,  k  e.  Top  |->  ( x  e.  U. j  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  (
( f `  x
)  e.  y  ->  E. g  e.  j 
( x  e.  g  /\  ( f "
g )  C_  y
) ) } ) )
Distinct variable group:    j, k, f, x, y, g

Detailed syntax breakdown of Definition df-cnp
StepHypRef Expression
1 ccnp 16882 . 2  class  CnP
2 vj . . 3  set  j
3 vk . . 3  set  k
4 ctop 16558 . . 3  class  Top
5 vx . . . 4  set  x
62cv 1618 . . . . 5  class  j
76cuni 3768 . . . 4  class  U. j
85cv 1618 . . . . . . . . 9  class  x
9 vf . . . . . . . . . 10  set  f
109cv 1618 . . . . . . . . 9  class  f
118, 10cfv 4638 . . . . . . . 8  class  ( f `
 x )
12 vy . . . . . . . . 9  set  y
1312cv 1618 . . . . . . . 8  class  y
1411, 13wcel 1621 . . . . . . 7  wff  ( f `
 x )  e.  y
15 vg . . . . . . . . . 10  set  g
165, 15wel 1622 . . . . . . . . 9  wff  x  e.  g
1715cv 1618 . . . . . . . . . . 11  class  g
1810, 17cima 4629 . . . . . . . . . 10  class  ( f
" g )
1918, 13wss 3094 . . . . . . . . 9  wff  ( f
" g )  C_  y
2016, 19wa 360 . . . . . . . 8  wff  ( x  e.  g  /\  (
f " g ) 
C_  y )
2120, 15, 6wrex 2517 . . . . . . 7  wff  E. g  e.  j  ( x  e.  g  /\  (
f " g ) 
C_  y )
2214, 21wi 6 . . . . . 6  wff  ( ( f `  x )  e.  y  ->  E. g  e.  j  ( x  e.  g  /\  (
f " g ) 
C_  y ) )
233cv 1618 . . . . . 6  class  k
2422, 12, 23wral 2516 . . . . 5  wff  A. y  e.  k  ( (
f `  x )  e.  y  ->  E. g  e.  j  ( x  e.  g  /\  (
f " g ) 
C_  y ) )
2523cuni 3768 . . . . . 6  class  U. k
26 cmap 6705 . . . . . 6  class  ^m
2725, 7, 26co 5757 . . . . 5  class  ( U. k  ^m  U. j )
2824, 9, 27crab 2519 . . . 4  class  { f  e.  ( U. k  ^m  U. j )  | 
A. y  e.  k  ( ( f `  x )  e.  y  ->  E. g  e.  j  ( x  e.  g  /\  ( f "
g )  C_  y
) ) }
295, 7, 28cmpt 4017 . . 3  class  ( x  e.  U. j  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  ( ( f `
 x )  e.  y  ->  E. g  e.  j  ( x  e.  g  /\  (
f " g ) 
C_  y ) ) } )
302, 3, 4, 4, 29cmpt2 5759 . 2  class  ( j  e.  Top ,  k  e.  Top  |->  ( x  e.  U. j  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  ( ( f `
 x )  e.  y  ->  E. g  e.  j  ( x  e.  g  /\  (
f " g ) 
C_  y ) ) } ) )
311, 30wceq 1619 1  wff  CnP  =  ( j  e.  Top ,  k  e.  Top  |->  ( x  e.  U. j  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  (
( f `  x
)  e.  y  ->  E. g  e.  j 
( x  e.  g  /\  ( f "
g )  C_  y
) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  cnpfval  16891  iscnp2  16896
  Copyright terms: Public domain W3C validator