Definition df-cn 7751

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 7755 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 7749	. 2 class Cn
2		vj	. . . . . . 7 set j
3	2	cv 957	. . . . . 6 class j
4		ctop 7590	. . . . . 6 class Top
5	3, 4	wcel 960	. . . . 5 wff j e. Top
6		vk	. . . . . . 7 set k
7	6	cv 957	. . . . . 6 class k
8	7, 4	wcel 960	. . . . 5 wff k e. Top
9	5, 8	wa 223	. . . 4 wff (j e. Top /\ k e. Top)
10		vz	. . . . . 6 set z
11	10	cv 957	. . . . 5 class z
12		vf	. . . . . . . . . . 11 set f
13	12	cv 957	. . . . . . . . . 10 class f
14	13	ccnv 3175	. . . . . . . . 9 class `'f
15		vy	. . . . . . . . . 10 set y
16	15	cv 957	. . . . . . . . 9 class y
17	14, 16	cima 3179	. . . . . . . 8 class (`'f"y)
18	17, 3	wcel 960	. . . . . . 7 wff (`'f"y) e. j
19	18, 15, 7	wral 1648	. . . . . 6 wff A.y e. k (`'f"y) e. j
20	7	cuni 2507	. . . . . . 7 class U.k
21	3	cuni 2507	. . . . . . 7 class U.j
22		cm 4328	. . . . . . 7 class ^m
23	20, 21, 22	co 3969	. . . . . 6 class (U.k ^m U.j)
24	19, 12, 23	crab 1651	. . . . 5 class {f e. (U.k ^m U.j) | A.y e. k (`'f"y) e. j}
25	11, 24	wceq 958	. . . 4 wff z = {f e. (U.k ^m U.j) | A.y e. k (`'f"y) e. j}
26	9, 25	wa 223	. . 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 3970	. 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 958	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 7753

Copyright terms: Public domain