Definition df-cn 9030

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 9034 for the predicate form.

Assertion

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

Distinct variable group:   f,j,k,y,z

Detailed syntax breakdown of Definition df-cn

Step	Hyp	Ref	Expression
1		ccn 9028	. 2 class Cn
2		vj	. . . . . . 7 set j
3	2	cv 1297	. . . . . 6 class j
4		ctop 8857	. . . . . 6 class Top
5	3, 4	wcel 1300	. . . . 5 wff j e. Top
6		vk	. . . . . . 7 set k
7	6	cv 1297	. . . . . 6 class k
8	7, 4	wcel 1300	. . . . 5 wff k e. Top
9	5, 8	wa 240	. . . 4 wff (j e. Top /\ k e. Top)
10		vz	. . . . . 6 set z
11	10	cv 1297	. . . . 5 class z
12		vf	. . . . . . . . . . 11 set f
13	12	cv 1297	. . . . . . . . . 10 class f
14	13	ccnv 3985	. . . . . . . . 9 class `'f
15		vy	. . . . . . . . . 10 set y
16	15	cv 1297	. . . . . . . . 9 class y
17	14, 16	cima 3989	. . . . . . . 8 class (`'f"y)
18	17, 3	wcel 1300	. . . . . . 7 wff (`'f"y) e. j
19	18, 15, 7	wral 2105	. . . . . 6 wff A.y e. k (`'f"y) e. j
20	7	cuni 3177	. . . . . . 7 class U.k
21	3	cuni 3177	. . . . . . 7 class U.j
22		cmap 5381	. . . . . . 7 class ^m
23	20, 21, 22	co 4884	. . . . . 6 class (U.k ^m U.j)
24	19, 12, 23	crab 2108	. . . . 5 class {f e. (U.k ^m U.j) | A.y e. k (`'f"y) e. j}
25	11, 24	wceq 1298	. . . 4 wff z = {f e. (U.k ^m U.j) | A.y e. k (`'f"y) e. j}
26	9, 25	wa 240	. . 3 wff ((j e. Top /\ k e. Top) /\ z = {f e. (U.k ^m U.j) | A.y e. k (`'f"y) e. j})
27	26, 2, 6, 10	copab2 4885	. 2 class {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {f e. (U.k ^m U.j) | A.y e. k (`'f"y) e. j})}
28	1, 27	wceq 1298	1 wff Cn = {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {f e. (U.k ^m U.j) | A.y e. k (`'f"y) e. j})}

This definition is referenced by:  cnfval 9032

Copyright terms: Public domain