Theorem cnpfval 7754

Description: The function mapping the points in a topology J to the set of all functions from J to topology K continuous at that point.

Hypotheses

Ref	Expression
cnfval.1	|- X = U.J
cnfval.2	|- Y = U.K

Assertion

Ref	Expression
cnpfval	|- ((J e. Top /\ K e. Top) -> (J CnP K) = {<.x, y>. | (x e. X /\ y = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})})

Distinct variable groups:   v,f,w,x,y,J   f,K,w,x,y   f,X,x,y   f,Y,y

Proof of Theorem cnpfval

Step	Hyp	Ref	Expression
1		uniexg 2877	. . . 4 |- (J e. Top -> U.J e. V)
2		cnfval.1	. . . . . 6 |- X = U.J
3	2	eleq1i 1540	. . . . 5 |- (X e. V <-> U.J e. V)
4	3	biimpr 152	. . . 4 |- (U.J e. V -> X e. V)
5		opabex2g 3617	. . . 4 |- (X e. V -> {<.x, y>. | (x e. X /\ y = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})} e. V)
6	1, 4, 5	3syl 20	. . 3 |- (J e. Top -> {<.x, y>. | (x e. X /\ y = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})} e. V)
7	6	adantr 391	. 2 |- ((J e. Top /\ K e. Top) -> {<.x, y>. | (x e. X /\ y = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})} e. V)
8		unieq 2514	. . . . . . 7 |- (j = J -> U.j = U.J)
9	8, 2	syl6eqr 1528	. . . . . 6 |- (j = J -> U.j = X)
10	9	eleq2d 1544	. . . . 5 |- (j = J -> (x e. U.j <-> x e. X))
11	9	opreq2d 3982	. . . . . . . 8 |- (j = J -> (U.k ^m U.j) = (U.k ^m X))
12		rabeq 1812	. . . . . . . 8 |- ((U.k ^m U.j) = (U.k ^m X) -> {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))} = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})
13	11, 12	syl 10	. . . . . . 7 |- (j = J -> {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))} = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})
14		rexeq1 1790	. . . . . . . . . 10 |- (j = J -> (E.v e. j (x e. v /\ (f"v) (_ w) <-> E.v e. J (x e. v /\ (f"v) (_ w)))
15	14	imbi2d 614	. . . . . . . . 9 |- (j = J -> (((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w)) <-> ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))))
16	15	ralbidv 1666	. . . . . . . 8 |- (j = J -> (A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w)) <-> A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))))
17	16	rabbisdv 1810	. . . . . . 7 |- (j = J -> {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))} = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})
18	13, 17	eqtrd 1510	. . . . . 6 |- (j = J -> {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))} = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})
19	18	eqeq2d 1489	. . . . 5 |- (j = 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))} <-> y = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))}))
20	10, 19	anbi12d 630	. . . 4 |- (j = J -> ((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))}) <-> (x e. X /\ y = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})))
21	20	opabbidv 2675	. . 3 |- (j = J -> {<.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))})} = {<.x, y>. | (x e. X /\ y = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})})
22		unieq 2514	. . . . . . . . . 10 |- (k = K -> U.k = U.K)
23		cnfval.2	. . . . . . . . . 10 |- Y = U.K
24	22, 23	syl6eqr 1528	. . . . . . . . 9 |- (k = K -> U.k = Y)
25	24	opreq1d 3981	. . . . . . . 8 |- (k = K -> (U.k ^m X) = (Y ^m X))
26		rabeq 1812	. . . . . . . 8 |- ((U.k ^m X) = (Y ^m X) -> {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))} = {f e. (Y ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})
27	25, 26	syl 10	. . . . . . 7 |- (k = K -> {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))} = {f e. (Y ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})
28		raleq1 1789	. . . . . . . 8 |- (k = K -> (A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w)) <-> A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))))
29	28	rabbisdv 1810	. . . . . . 7 |- (k = K -> {f e. (Y ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))} = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})
30	27, 29	eqtrd 1510	. . . . . 6 |- (k = K -> {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))} = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})
31	30	eqeq2d 1489	. . . . 5 |- (k = K -> (y = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))} <-> y = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))}))
32	31	anbi2d 618	. . . 4 |- (k = K -> ((x e. X /\ y = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))}) <-> (x e. X /\ y = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})))
33	32	opabbidv 2675	. . 3 |- (k = K -> {<.x, y>. | (x e. X /\ y = {f e. (U.k ^m X) | A.w e. k ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})} = {<.x, y>. | (x e. X /\ y = {f e. (Y ^m X) | A.w e. K ((f` x) e. w -> E.v e. J (x e. v /\ (f"v) (_ w))})})
34