Definition df-cn 14508

Description: Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p. 102. See iscn 14517 for the predicate form. (Contributed by NM, 17-Oct-2006.)

Assertion

Ref	Expression
df-cn	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )

Distinct variable group:   j, k, f, y

Detailed syntax breakdown of Definition df-cn

Step	Hyp	Ref	Expression
1		ccn 14505	. 2 class Cn
2		vj	. . 3 setvar j
3		vk	. . 3 setvar k
4		ctop 14317	. . 3 class Top
5		vf	. . . . . . . . 9 setvar f
6	5	cv 1363	. . . . . . . 8 class f
7	6	ccnv 4663	. . . . . . 7 class `' f
8		vy	. . . . . . . 8 setvar y
9	8	cv 1363	. . . . . . 7 class y
10	7, 9	cima 4667	. . . . . 6 class ( `' f " y )
11	2	cv 1363	. . . . . 6 class j
12	10, 11	wcel 2167	. . . . 5 wff ( `' f " y ) e. j
13	3	cv 1363	. . . . 5 class k
14	12, 8, 13	wral 2475	. . . 4 wff A. y e. k ( `' f " y ) e. j
15	13	cuni 3840	. . . . 5 class U. k
16	11	cuni 3840	. . . . 5 class U. j
17		cmap 6716	. . . . 5 class ^m
18	15, 16, 17	co 5925	. . . 4 class ( U. k ^m U. j )
19	14, 5, 18	crab 2479	. . 3 class { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j }
20	2, 3, 4, 4, 19	cmpo 5927	. 2 class ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
21	1, 20	wceq 1364	1 wff Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )

This definition is referenced by:  cnfval  14514  iscn2  14520  ishmeo  14624