Step |
Hyp |
Ref |
Expression |
1 |
|
negcncf.1 |
|- F = ( x e. A |-> -u x ) |
2 |
|
ssel2 |
|- ( ( A C_ CC /\ x e. A ) -> x e. CC ) |
3 |
2
|
mulm1d |
|- ( ( A C_ CC /\ x e. A ) -> ( -u 1 x. x ) = -u x ) |
4 |
3
|
mpteq2dva |
|- ( A C_ CC -> ( x e. A |-> ( -u 1 x. x ) ) = ( x e. A |-> -u x ) ) |
5 |
4 1
|
eqtr4di |
|- ( A C_ CC -> ( x e. A |-> ( -u 1 x. x ) ) = F ) |
6 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
7 |
6
|
mulcn |
|- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) |
8 |
7
|
a1i |
|- ( A C_ CC -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) ) |
9 |
|
neg1cn |
|- -u 1 e. CC |
10 |
|
ssid |
|- CC C_ CC |
11 |
|
cncfmptc |
|- ( ( -u 1 e. CC /\ A C_ CC /\ CC C_ CC ) -> ( x e. A |-> -u 1 ) e. ( A -cn-> CC ) ) |
12 |
9 10 11
|
mp3an13 |
|- ( A C_ CC -> ( x e. A |-> -u 1 ) e. ( A -cn-> CC ) ) |
13 |
|
cncfmptid |
|- ( ( A C_ CC /\ CC C_ CC ) -> ( x e. A |-> x ) e. ( A -cn-> CC ) ) |
14 |
10 13
|
mpan2 |
|- ( A C_ CC -> ( x e. A |-> x ) e. ( A -cn-> CC ) ) |
15 |
6 8 12 14
|
cncfmpt2f |
|- ( A C_ CC -> ( x e. A |-> ( -u 1 x. x ) ) e. ( A -cn-> CC ) ) |
16 |
5 15
|
eqeltrrd |
|- ( A C_ CC -> F e. ( A -cn-> CC ) ) |