Definition df-cnp 13728

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 13725	. 2 class CnP
2		vj	. . 3 setvar j
3		vk	. . 3 setvar k
4		ctop 13536	. . 3 class Top
5		vx	. . . 4 setvar x
6	2	cv 1352	. . . . 5 class j
7	6	cuni 3811	. . . 4 class U. j
8	5	cv 1352	. . . . . . . . 9 class x
9		vf	. . . . . . . . . 10 setvar f
10	9	cv 1352	. . . . . . . . 9 class f
11	8, 10	cfv 5218	. . . . . . . 8 class ( f ` x )
12		vy	. . . . . . . . 9 setvar y
13	12	cv 1352	. . . . . . . 8 class y
14	11, 13	wcel 2148	. . . . . . 7 wff ( f ` x ) e. y
15		vg	. . . . . . . . . 10 setvar g
16	5, 15	wel 2149	. . . . . . . . 9 wff x e. g
17	15	cv 1352	. . . . . . . . . . 11 class g
18	10, 17	cima 4631	. . . . . . . . . 10 class ( f " g )
19	18, 13	wss 3131	. . . . . . . . 9 wff ( f " g ) C_ y
20	16, 19	wa 104	. . . . . . . 8 wff ( x e. g /\ ( f " g ) C_ y )
21	20, 15, 6	wrex 2456	. . . . . . 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 1352	. . . . . 6 class k
24	22, 12, 23	wral 2455	. . . . 5 wff A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) )
25	23	cuni 3811	. . . . . 6 class U. k
26		cmap 6650	. . . . . 6 class ^m
27	25, 7, 26	co 5877	. . . . 5 class ( U. k ^m U. j )
28	24, 9, 27	crab 2459	. . . 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 4066	. . 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 5879	. 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 1353	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  13734  cnprcl2k  13745