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 ) ) )