Step |
Hyp |
Ref |
Expression |
1 |
|
sub1cncf.1 |
|- F = ( x e. CC |-> ( x - A ) ) |
2 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
3 |
2
|
subcn |
|- - 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 |
|
eqid |
|- ( x e. CC |-> x ) = ( x e. CC |-> x ) |
6 |
5
|
idcncf |
|- ( x e. CC |-> x ) e. ( CC -cn-> CC ) |
7 |
6
|
a1i |
|- ( A e. CC -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) ) |
8 |
|
ssid |
|- CC C_ CC |
9 |
|
cncfmptc |
|- ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) ) |
10 |
8 8 9
|
mp3an23 |
|- ( A e. CC -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) ) |
11 |
2 4 7 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 ) ) |