This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordtrestixx

Description: The restriction of the less than order to an interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordtrestixx.1 
|- A C_ RR*
ordtrestixx.2 
|- ( ( x e. A /\ y e. A ) -> ( x [,] y ) C_ A )
Assertion ordtrestixx 
|- ( ( ordTop ` <_ ) |`t A ) = ( ordTop ` ( <_ i^i ( A X. A ) ) )

Proof

Step Hyp Ref Expression
1 ordtrestixx.1 
 |-  A C_ RR*
2 ordtrestixx.2 
 |-  ( ( x e. A /\ y e. A ) -> ( x [,] y ) C_ A )
3 ledm 
 |-  RR* = dom <_
4 letsr 
 |-  <_ e. TosetRel
5 4 a1i 
 |-  ( T. -> <_ e. TosetRel )
6 1 a1i 
 |-  ( T. -> A C_ RR* )
7 1 sseli 
 |-  ( x e. A -> x e. RR* )
8 1 sseli 
 |-  ( y e. A -> y e. RR* )
9 iccval 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x [,] y ) = { z e. RR* | ( x <_ z /\ z <_ y ) } )
10 7 8 9 syl2an 
 |-  ( ( x e. A /\ y e. A ) -> ( x [,] y ) = { z e. RR* | ( x <_ z /\ z <_ y ) } )
11 10 2 eqsstrrd 
 |-  ( ( x e. A /\ y e. A ) -> { z e. RR* | ( x <_ z /\ z <_ y ) } C_ A )
12 11 adantl 
 |-  ( ( T. /\ ( x e. A /\ y e. A ) ) -> { z e. RR* | ( x <_ z /\ z <_ y ) } C_ A )
13 3 5 6 12 ordtrest2 
 |-  ( T. -> ( ordTop ` ( <_ i^i ( A X. A ) ) ) = ( ( ordTop ` <_ ) |`t A ) )
14 13 eqcomd 
 |-  ( T. -> ( ( ordTop ` <_ ) |`t A ) = ( ordTop ` ( <_ i^i ( A X. A ) ) ) )
15 14 mptru 
 |-  ( ( ordTop ` <_ ) |`t A ) = ( ordTop ` ( <_ i^i ( A X. A ) ) )