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 = ( 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 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnp 
 |-  CnP
1 vj 
 |-  j
2 ctop 
 |-  Top
3 vk 
 |-  k
4 vx 
 |-  x
5 1 cv 
 |-  j
6 5 cuni 
 |-  U. j
7 vf 
 |-  f
8 3 cv 
 |-  k
9 8 cuni 
 |-  U. k
10 cmap 
 |-  ^m
11 9 6 10 co 
 |-  ( U. k ^m U. j )
12 vy 
 |-  y
13 7 cv 
 |-  f
14 4 cv 
 |-  x
15 14 13 cfv 
 |-  ( f ` x )
16 12 cv 
 |-  y
17 15 16 wcel 
 |-  ( f ` x ) e. y
18 vg 
 |-  g
19 18 cv 
 |-  g
20 14 19 wcel 
 |-  x e. g
21 13 19 cima 
 |-  ( f " g )
22 21 16 wss 
 |-  ( f " g ) C_ y
23 20 22 wa 
 |-  ( x e. g /\ ( f " g ) C_ y )
24 23 18 5 wrex 
 |-  E. g e. j ( x e. g /\ ( f " g ) C_ y )
25 17 24 wi 
 |-  ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) )
26 25 12 8 wral 
 |-  A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) )
27 26 7 11 crab 
 |-  { 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 ) ) }
28 4 6 27 cmpt 
 |-  ( 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 ) ) } )
29 1 3 2 2 28 cmpo 
 |-  ( 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 ) ) } ) )
30 0 29 wceq 
 |-  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 ) ) } ) )