Step |
Hyp |
Ref |
Expression |
1 |
|
cdivcncf.1 |
|- F = ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) |
2 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
3 |
2
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
4 |
3
|
a1i |
|- ( A e. CC -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) |
5 |
|
difss |
|- ( CC \ { 0 } ) C_ CC |
6 |
|
resttopon |
|- ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) ) |
7 |
4 5 6
|
sylancl |
|- ( A e. CC -> ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) ) |
8 |
|
id |
|- ( A e. CC -> A e. CC ) |
9 |
7 4 8
|
cnmptc |
|- ( A e. CC -> ( x e. ( CC \ { 0 } ) |-> A ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) ) |
10 |
7
|
cnmptid |
|- ( A e. CC -> ( x e. ( CC \ { 0 } ) |-> x ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) ) |
11 |
|
eqid |
|- ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) |
12 |
2 11
|
divcn |
|- / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) ) |
13 |
12
|
a1i |
|- ( A e. CC -> / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) ) ) |
14 |
7 9 10 13
|
cnmpt12f |
|- ( A e. CC -> ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) ) |
15 |
|
ssid |
|- CC C_ CC |
16 |
3
|
toponrestid |
|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC ) |
17 |
2 11 16
|
cncfcn |
|- ( ( ( CC \ { 0 } ) C_ CC /\ CC C_ CC ) -> ( ( CC \ { 0 } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) ) |
18 |
5 15 17
|
mp2an |
|- ( ( CC \ { 0 } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) |
19 |
14 1 18
|
3eltr4g |
|- ( A e. CC -> F e. ( ( CC \ { 0 } ) -cn-> CC ) ) |