Step |
Hyp |
Ref |
Expression |
1 |
|
tgioo3.1 |
|- J = ( TopOpen ` RRfld ) |
2 |
|
eqid |
|- ( CCfld |`s RR ) = ( CCfld |`s RR ) |
3 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
4 |
2 3
|
resstopn |
|- ( ( TopOpen ` CCfld ) |`t RR ) = ( TopOpen ` ( CCfld |`s RR ) ) |
5 |
3
|
tgioo2 |
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
6 |
|
df-refld |
|- RRfld = ( CCfld |`s RR ) |
7 |
6
|
fveq2i |
|- ( TopOpen ` RRfld ) = ( TopOpen ` ( CCfld |`s RR ) ) |
8 |
1 7
|
eqtri |
|- J = ( TopOpen ` ( CCfld |`s RR ) ) |
9 |
4 5 8
|
3eqtr4i |
|- ( topGen ` ran (,) ) = J |