Description: The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xrstopn | |- ( ordTop ` <_ ) = ( TopOpen ` RR*s ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | letopon | |- ( ordTop ` <_ ) e. ( TopOn ` RR* ) |
|
2 | xrsbas | |- RR* = ( Base ` RR*s ) |
|
3 | xrstset | |- ( ordTop ` <_ ) = ( TopSet ` RR*s ) |
|
4 | 2 3 | topontopn | |- ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) -> ( ordTop ` <_ ) = ( TopOpen ` RR*s ) ) |
5 | 1 4 | ax-mp | |- ( ordTop ` <_ ) = ( TopOpen ` RR*s ) |