Theorem cncfval 7264

Description: The value of the continuous complex function operation is the set of continuous functions from A to B. (Contributed by Paul Chapman, 11-Oct-2007.)

Assertion

Ref	Expression
cncfval	|- ((A (_ CC /\ B (_ CC) -> (A-cn->B) = {f | (f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})

Distinct variable groups:   A,f,w,x,y,z   B,f

Proof of Theorem cncfval

Step	Hyp	Ref	Expression
1		axcnex 5279	. . 3 |- CC e. V
2		elpw2g 2732	. . . 4 |- (CC e. V -> (A e. P~CC <-> A (_ CC))
3		elpw2g 2732	. . . 4 |- (CC e. V -> (B e. P~CC <-> B (_ CC))
4	2, 3	anbi12d 630	. . 3 |- (CC e. V -> ((A e. P~CC /\ B e. P~CC) <-> (A (_ CC /\ B (_ CC)))
5	1, 4	ax-mp 7	. 2 |- ((A e. P~CC /\ B e. P~CC) <-> (A (_ CC /\ B (_ CC))
6		mapex 4334	. . . 4 |- ((A e. P~CC /\ B e. P~CC) -> {f | f:A-->B} e. V)
7		pm3.26 319	. . . . . 6 |- ((f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)) -> f:A-->B)
8	7	ss2abi 2123	. . . . 5 |- {f | (f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))} (_ {f | f:A-->B}
9		ssexg 2726	. . . . 5 |- (({f | (f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))} (_ {f | f:A-->B} /\ {f | f:A-->B} e. V) -> {f | (f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))} e. V)
10	8, 9	mpan 697	. . . 4 |- ({f | f:A-->B} e. V -> {f | (f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))} e. V)
11	6, 10	syl 10	. . 3 |- ((A e. P~CC /\ B e. P~CC) -> {f | (f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))} e. V)
12		feq2 3627	. . . . . 6 |- (a = A -> (f:a-->b <-> f:A-->b))
13		raleq1 1789	. . . . . . . . 9 |- (a = A -> (A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y) <-> A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)))
14	13	rexbidv 1667	. . . . . . . 8 |- (a = A -> (E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y) <-> E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)))
15	14	ralbidv 1666	. . . . . . 7 |- (a = A -> (A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y) <-> A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)))
16	15	raleqd 1794	. . . . . 6 |- (a = A -> (A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y) <-> A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)))
17	12, 16	anbi12d 630	. . . . 5 |- (a = A -> ((f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)) <-> (f:A-->b /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))))
18	17	abbidv 1580	. . . 4 |- (a = A -> {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))} = {f | (f:A-->b /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})
19		feq3 3628	. . . . . 6 |- (b = B -> (f:A-->b <-> f:A-->B))
20	19	anbi1d 619	. . . . 5 |- (b = B -> ((f:A-->b /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)) <-> (f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))))
21	20	abbidv 1580	. . . 4 |- (b = B -> {f | (f:A-->b /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))} = {f | (f:A-->B /\ A.x e. A A.y e. RR+ E.z e. RR+ A.w e. A ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})
22		df-cncf 7263	. . . . 5 |- -cn-> = {<.<.a, b>., s>. | ((a (_ CC /\ b (_ CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})}
23		elpw2g 2732	. . . . . . . . 9 |- (CC e. V -> (a e. P~CC <-> a (_ CC))
24		elpw2g 2732	. . . . . . . . 9 |- (CC e. V -> (b e. P~CC <-> b (_ CC))
25	23, 24	anbi12d 630	. . . . . . . 8 |- (CC e. V -> ((a e. P~CC /\ b e. P~CC) <-> (a (_ CC /\ b (_ CC)))
26	1, 25	ax-mp 7	. . . . . . 7 |- ((a e. P~CC /\ b e. P~CC) <-> (a (_ CC /\ b (_ CC))
27	26	anbi1i 483	. . . . . 6 |- (((a e. P~CC /\ b e. P~CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))}) <-> ((a (_ CC /\ b (_ CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))}))
28	27	oprabbii 4003	. . . . 5 |- {<.<.a, b>., s>. | ((a e. P~CC /\ b e. P~CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})} = {<.<.a, b>., s>. | ((a (_ CC /\ b (_ CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})}
29	22, 28	eqtr4 1501	. . . 4 |- -cn-> = {<.<.a, b>., s>. | ((a e. P~CC /\