Definition df-cnp 7755

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.

Assertion

Ref	Expression
df-cnp	|- CnP = {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {<.x, y>. | (x e. U.j /\ y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})})}

Distinct variable group:   f,j,k,v,w,x,y,z

Detailed syntax breakdown of Definition df-cnp

Step	Hyp	Ref	Expression
1		ccnp 7753	. 2 class CnP
2		vj	. . . . . . 7 set j
3	2	cv 955	. . . . . 6 class j
4		ctop 7588	. . . . . 6 class Top
5	3, 4	wcel 958	. . . . 5 wff j e. Top
6		vk	. . . . . . 7 set k
7	6	cv 955	. . . . . 6 class k
8	7, 4	wcel 958	. . . . 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 955	. . . . 5 class z
12		vx	. . . . . . . . 9 set x
13	12	cv 955	. . . . . . . 8 class x
14	3	cuni 2503	. . . . . . . 8 class U.j
15	13, 14	wcel 958	. . . . . . 7 wff x e. U.j
16		vy	. . . . . . . . 9 set y
17	16	cv 955	. . . . . . . 8 class y
18		vf	. . . . . . . . . . . . . 14 set f
19	18	cv 955	. . . . . . . . . . . . 13 class f
20	13, 19	cfv 3182	. . . . . . . . . . . 12 class (f` x)
21		vw	. . . . . . . . . . . . 13 set w
22	21	cv 955	. . . . . . . . . . . 12 class w
23	20, 22	wcel 958	. . . . . . . . . . 11 wff (f` x) e. w
24		vv	. . . . . . . . . . . . . . 15 set v
25	24	cv 955	. . . . . . . . . . . . . 14 class v
26	13, 25	wcel 958	. . . . . . . . . . . . 13 wff x e. v
27	19, 25	cima 3173	. . . . . . . . . . . . . 14 class (f"v)
28	27, 22	wss 2047	. . . . . . . . . . . . 13 wff (f"v) (_ w
29	26, 28	wa 223	. . . . . . . . . . . 12 wff (x e. v /\ (f"v) (_ w)
30	29, 24, 3	wrex 1646	. . . . . . . . . . 11 wff E.v e. j (x e. v /\ (f"v) (_ w)
31	23, 30	wi 3	. . . . . . . . . 10 wff ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))
32	31, 21, 7	wral 1645	. . . . . . . . 9 wff A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))
33	7	cuni 2503	. . . . . . . . . 10 class U.k
34		cm 4322	. . . . . . . . . 10 class ^m
35	33, 14, 34	co 3963	. . . . . . . . 9 class (U.k ^m U.j)
36	32, 18, 35	crab 1648	. . . . . . . 8 class {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))}
37	17, 36	wceq 956	. . . . . . 7 wff y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))}
38	15, 37	wa 223	. . . . . 6 wff (x e. U.j /\ y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})
39	38, 12, 16	copab 2666	. . . . 5 class {<.x, y>. | (x e. U.j /\ y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})}
40	11, 39	wceq 956	. . . 4 wff z = {<.x, y>. | (x e. U.j /\ y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})}
41	9, 40	wa 223	. . 3 wff ((j e. Top /\ k e. Top) /\ z = {<.x, y>. | (x e. U.j /\ y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})})
42	41, 2, 6, 10	copab2 3964	. 2 class {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {<.x, y>. | (x e. U.j /\ y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})})}
43	1, 42	wceq 956	1 wff CnP = {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {<.x, y>. | (x e. U.j /\ y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})})}

This definition is referenced by:  cnpfval 7757

Copyright terms: Public domain