Definition df-cnp 12829

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

Step	Hyp	Ref	Expression
1		ccnp 12826	. 2 class CnP
2		vj	. . 3 setvar j
3		vk	. . 3 setvar k
4		ctop 12635	. . 3 class Top
5		vx	. . . 4 setvar x
6	2	cv 1342	. . . . 5 class j
7	6	cuni 3789	. . . 4 class U. j
8	5	cv 1342	. . . . . . . . 9 class x
9		vf	. . . . . . . . . 10 setvar f
10	9	cv 1342	. . . . . . . . 9 class f
11	8, 10	cfv 5188	. . . . . . . 8 class ( f ` x )
12		vy	. . . . . . . . 9 setvar y
13	12	cv 1342	. . . . . . . 8 class y
14	11, 13	wcel 2136	. . . . . . 7 wff ( f ` x ) e. y
15		vg	. . . . . . . . . 10 setvar g
16	5, 15	wel 2137	. . . . . . . . 9 wff x e. g
17	15	cv 1342	. . . . . . . . . . 11 class g
18	10, 17	cima 4607	. . . . . . . . . 10 class ( f " g )
19	18, 13	wss 3116	. . . . . . . . 9 wff ( f " g ) C_ y
20	16, 19	wa 103	. . . . . . . 8 wff ( x e. g /\ ( f " g ) C_ y )
21	20, 15, 6	wrex 2445	. . . . . . 7 wff E. g e. j ( x e. g /\ ( f " g ) C_ y )
22	14, 21	wi 4	. . . . . 6 wff ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) )
23	3	cv 1342	. . . . . 6 class k
24	22, 12, 23	wral 2444	. . . . 5 wff A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) )
25	23	cuni 3789	. . . . . 6 class U. k
26		cmap 6614	. . . . . 6 class ^m
27	25, 7, 26	co 5842	. . . . 5 class ( U. k ^m U. j )
28	24, 9, 27	crab 2448	. . . 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 ) ) }
29	5, 7, 28	cmpt 4043	. . 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 ) ) } )
30	2, 3, 4, 4, 29	cmpo 5844	. 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 ) ) } ) )
31	1, 30	wceq 1343	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 ) ) } ) )

This definition is referenced by:  cnpfval  12835  cnprcl2k  12846