Metamath Proof Explorer

Theorem cnvordtrestixx

Description: The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 cnvordtrestixx.1 
 |-  A C_ RR*
2 cnvordtrestixx.2 
 |-  ( ( x e. A /\ y e. A ) -> ( x [,] y ) C_ A )
3 lern 
 |-  RR* = ran <_
4 df-rn 
 |-  ran <_ = dom `' <_
5 3 4 eqtri 
 |-  RR* = dom `' <_
6 letsr 
 |-  <_ e. TosetRel
7 cnvtsr 
 |-  ( <_ e. TosetRel -> `' <_ e. TosetRel )
8 6 7 ax-mp 
 |-  `' <_ e. TosetRel
9 8 a1i 
 |-  ( T. -> `' <_ e. TosetRel )
10 1 a1i 
 |-  ( T. -> A C_ RR* )
11 brcnvg 
 |-  ( ( y e. A /\ z e. RR* ) -> ( y `' <_ z <-> z <_ y ) )
12 11 adantlr 
 |-  ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> ( y `' <_ z <-> z <_ y ) )
13 simpr 
 |-  ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> z e. RR* )
14 simplr 
 |-  ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> x e. A )
15 brcnvg 
 |-  ( ( z e. RR* /\ x e. A ) -> ( z `' <_ x <-> x <_ z ) )
16 13 14 15 syl2anc 
 |-  ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> ( z `' <_ x <-> x <_ z ) )
17 12 16 anbi12d 
 |-  ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> ( ( y `' <_ z /\ z `' <_ x ) <-> ( z <_ y /\ x <_ z ) ) )
18 ancom 
 |-  ( ( z <_ y /\ x <_ z ) <-> ( x <_ z /\ z <_ y ) )
19 17 18 bitrdi 
 |-  ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> ( ( y `' <_ z /\ z `' <_ x ) <-> ( x <_ z /\ z <_ y ) ) )
20 19 rabbidva 
 |-  ( ( y e. A /\ x e. A ) -> { z e. RR* | ( y `' <_ z /\ z `' <_ x ) } = { z e. RR* | ( x <_ z /\ z <_ y ) } )
21 simpr 
 |-  ( ( y e. A /\ x e. A ) -> x e. A )
22 1 21 sselid 
 |-  ( ( y e. A /\ x e. A ) -> x e. RR* )
23 simpl 
 |-  ( ( y e. A /\ x e. A ) -> y e. A )
24 1 23 sselid 
 |-  ( ( y e. A /\ x e. A ) -> y e. RR* )
25 iccval 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x [,] y ) = { z e. RR* | ( x <_ z /\ z <_ y ) } )
26 22 24 25 syl2anc 
 |-  ( ( y e. A /\ x e. A ) -> ( x [,] y ) = { z e. RR* | ( x <_ z /\ z <_ y ) } )
27 2 ancoms 
 |-  ( ( y e. A /\ x e. A ) -> ( x [,] y ) C_ A )
28 26 27 eqsstrrd 
 |-  ( ( y e. A /\ x e. A ) -> { z e. RR* | ( x <_ z /\ z <_ y ) } C_ A )
29 20 28 eqsstrd 
 |-  ( ( y e. A /\ x e. A ) -> { z e. RR* | ( y `' <_ z /\ z `' <_ x ) } C_ A )
30 29 adantl 
 |-  ( ( T. /\ ( y e. A /\ x e. A ) ) -> { z e. RR* | ( y `' <_ z /\ z `' <_ x ) } C_ A )
31 5 9 10 30 ordtrest2 
 |-  ( T. -> ( ordTop ` ( `' <_ i^i ( A X. A ) ) ) = ( ( ordTop ` `' <_ ) |`t A ) )
32 31 mptru 
 |-  ( ordTop ` ( `' <_ i^i ( A X. A ) ) ) = ( ( ordTop ` `' <_ ) |`t A )
33 tsrps 
 |-  ( <_ e. TosetRel -> <_ e. PosetRel )
34 6 33 ax-mp 
 |-  <_ e. PosetRel
35 ordtcnv 
 |-  ( <_ e. PosetRel -> ( ordTop ` `' <_ ) = ( ordTop ` <_ ) )
36 34 35 ax-mp 
 |-  ( ordTop ` `' <_ ) = ( ordTop ` <_ )
37 36 oveq1i 
 |-  ( ( ordTop ` `' <_ ) |`t A ) = ( ( ordTop ` <_ ) |`t A )
38 32 37 eqtr2i 
 |-  ( ( ordTop ` <_ ) |`t A ) = ( ordTop ` ( `' <_ i^i ( A X. A ) ) )