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 *
ordtrestixx.2 x A y A x y A
Assertion ordtrestixx ordTop 𝑡 A = ordTop A × A

Proof

Step Hyp Ref Expression
1 ordtrestixx.1 A *
2 ordtrestixx.2 x A y A x y A
3 ledm * = dom
4 letsr TosetRel
5 4 a1i TosetRel
6 1 a1i A *
7 1 sseli x A x *
8 1 sseli y A y *
9 iccval x * y * x y = z * | x z z y
10 7 8 9 syl2an x A y A x y = z * | x z z y
11 10 2 eqsstrrd x A y A z * | x z z y A
12 11 adantl x A y A z * | x z z y A
13 3 5 6 12 ordtrest2 ordTop A × A = ordTop 𝑡 A
14 13 eqcomd ordTop 𝑡 A = ordTop A × A
15 14 mptru ordTop 𝑡 A = ordTop A × A