HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cncfval 7199
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
StepHypRef Expression
1 axcnex 5239 . . 3 |- CC e. V
2 elpw2g 2717 . . . 4 |- (CC e. V -> (A e. P~CC <-> A (_ CC))
3 elpw2g 2717 . . . 4 |- (CC e. V -> (B e. P~CC <-> B (_ CC))
42, 3anbi12d 626 . . 3 |- (CC e. V -> ((A e. P~CC /\ B e. P~CC) <-> (A (_ CC /\ B (_ CC)))
51, 4ax-mp 7 . 2 |- ((A e. P~CC /\ B e. P~CC) <-> (A (_ CC /\ B (_ CC))
6 mapex 4312 . . . 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)
87ss2abi 2110 . . . . 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 2711 . . . . 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)
108, 9mpan 693 . . . 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)
116, 10syl 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 3607 . . . . . 6 |- (a = A -> (f:a-->b <-> f:A-->b))
13 raleq1 1778 . . . . . . . . 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)))
1413rexbidv 1656 . . . . . . . 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)))
1514ralbidv 1655 . . . . . . 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)))
1615raleqd 1783 . . . . . 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)))
1712, 16anbi12d 626 . . . . 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))))
1817abbidv 1569 . . . 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 3608 . . . . . 6 |- (b = B -> (f:A-->b <-> f:A-->B))
2019anbi1d 615 . . . . 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))))
2120abbidv 1569 . . . 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 7198 . . . . 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 2717 . . . . . . . . 9 |- (CC e. V -> (a e. P~CC <-> a (_ CC))
24 elpw2g 2717 . . . . . . . . 9 |- (CC e. V -> (b e. P~CC <-> b (_ CC))
2523, 24anbi12d 626 . . . . . . . 8 |- (CC e. V -> ((a e. P~CC /\ b e. P~CC) <-> (a (_ CC /\ b (_ CC)))
261, 25ax-mp 7 . . . . . . 7 |- ((a e. P~CC /\ b e. P~CC) <-> (a (_ CC /\ b (_ CC))
2726anbi1i 480 . . . . . 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))}))
2827oprabbii 3982 . . . . 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))})}
2922, 28eqtr4 1490 . . . 4 |- -cn-> = {<.<.a, b>., s>. | ((a e. P~CC /\ b