Step |
Hyp |
Ref |
Expression |
1 |
|
coscn |
|- cos e. ( CC -cn-> CC ) |
2 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
3 |
2
|
cncfcn1 |
|- ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) |
4 |
1 3
|
eleqtri |
|- cos e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) |
5 |
2
|
cnfldhaus |
|- ( TopOpen ` CCfld ) e. Haus |
6 |
|
0cn |
|- 0 e. CC |
7 |
2
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
8 |
7
|
toponunii |
|- CC = U. ( TopOpen ` CCfld ) |
9 |
8
|
sncld |
|- ( ( ( TopOpen ` CCfld ) e. Haus /\ 0 e. CC ) -> { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) ) ) |
10 |
5 6 9
|
mp2an |
|- { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) ) |
11 |
8
|
cldopn |
|- ( { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) ) -> ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) ) |
12 |
10 11
|
ax-mp |
|- ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) |
13 |
|
cnima |
|- ( ( cos e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) /\ ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) ) -> ( `' cos " ( CC \ { 0 } ) ) e. ( TopOpen ` CCfld ) ) |
14 |
4 12 13
|
mp2an |
|- ( `' cos " ( CC \ { 0 } ) ) e. ( TopOpen ` CCfld ) |