Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
2 |
|
eqid |
|- ( topGen ` ran (,) ) = ( topGen ` ran (,) ) |
3 |
1 2
|
abscn |
|- abs e. ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) ) |
4 |
|
ssid |
|- CC C_ CC |
5 |
|
ax-resscn |
|- RR C_ CC |
6 |
1
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
7 |
6
|
toponunii |
|- CC = U. ( TopOpen ` CCfld ) |
8 |
7
|
restid |
|- ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) ) |
9 |
6 8
|
ax-mp |
|- ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) |
10 |
9
|
eqcomi |
|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC ) |
11 |
1
|
tgioo2 |
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
12 |
1 10 11
|
cncfcn |
|- ( ( CC C_ CC /\ RR C_ CC ) -> ( CC -cn-> RR ) = ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) ) ) |
13 |
4 5 12
|
mp2an |
|- ( CC -cn-> RR ) = ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) ) |
14 |
3 13
|
eleqtrri |
|- abs e. ( CC -cn-> RR ) |