Step |
Hyp |
Ref |
Expression |
1 |
|
negfcncf.1 |
|- G = ( x e. A |-> -u ( F ` x ) ) |
2 |
|
cncff |
|- ( F e. ( A -cn-> CC ) -> F : A --> CC ) |
3 |
2
|
ffvelrnda |
|- ( ( F e. ( A -cn-> CC ) /\ x e. A ) -> ( F ` x ) e. CC ) |
4 |
2
|
feqmptd |
|- ( F e. ( A -cn-> CC ) -> F = ( x e. A |-> ( F ` x ) ) ) |
5 |
|
eqidd |
|- ( F e. ( A -cn-> CC ) -> ( y e. CC |-> -u y ) = ( y e. CC |-> -u y ) ) |
6 |
|
negeq |
|- ( y = ( F ` x ) -> -u y = -u ( F ` x ) ) |
7 |
3 4 5 6
|
fmptco |
|- ( F e. ( A -cn-> CC ) -> ( ( y e. CC |-> -u y ) o. F ) = ( x e. A |-> -u ( F ` x ) ) ) |
8 |
7 1
|
eqtr4di |
|- ( F e. ( A -cn-> CC ) -> ( ( y e. CC |-> -u y ) o. F ) = G ) |
9 |
|
id |
|- ( F e. ( A -cn-> CC ) -> F e. ( A -cn-> CC ) ) |
10 |
|
ssid |
|- CC C_ CC |
11 |
|
eqid |
|- ( y e. CC |-> -u y ) = ( y e. CC |-> -u y ) |
12 |
11
|
negcncf |
|- ( CC C_ CC -> ( y e. CC |-> -u y ) e. ( CC -cn-> CC ) ) |
13 |
10 12
|
mp1i |
|- ( F e. ( A -cn-> CC ) -> ( y e. CC |-> -u y ) e. ( CC -cn-> CC ) ) |
14 |
9 13
|
cncfco |
|- ( F e. ( A -cn-> CC ) -> ( ( y e. CC |-> -u y ) o. F ) e. ( A -cn-> CC ) ) |
15 |
8 14
|
eqeltrrd |
|- ( F e. ( A -cn-> CC ) -> G e. ( A -cn-> CC ) ) |