Step |
Hyp |
Ref |
Expression |
1 |
|
addccncf.1 |
|- F = ( x e. CC |-> ( x + A ) ) |
2 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
3 |
2
|
addcn |
|- + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) |
4 |
3
|
a1i |
|- ( A e. CC -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) ) |
5 |
|
ssid |
|- CC C_ CC |
6 |
|
cncfmptid |
|- ( ( CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) ) |
7 |
5 5 6
|
mp2an |
|- ( x e. CC |-> x ) e. ( CC -cn-> CC ) |
8 |
7
|
a1i |
|- ( A e. CC -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) ) |
9 |
|
cncfmptc |
|- ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) ) |
10 |
5 5 9
|
mp3an23 |
|- ( A e. CC -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) ) |
11 |
2 4 8 10
|
cncfmpt2f |
|- ( A e. CC -> ( x e. CC |-> ( x + A ) ) e. ( CC -cn-> CC ) ) |
12 |
1 11
|
eqeltrid |
|- ( A e. CC -> F e. ( CC -cn-> CC ) ) |