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\subseteq {ℝ}^{*}$$
	ordtrestixx.2	$$⊢\left(x\in A\wedge y\in A\right)\to \left[x,y\right]\subseteq A$$
Assertion	ordtrestixx	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}A=\mathrm{ordTop}\left(\le \cap \left(A\times A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordtrestixx.1	$$⊢A\subseteq {ℝ}^{*}$$
2		ordtrestixx.2	$$⊢\left(x\in A\wedge y\in A\right)\to \left[x,y\right]\subseteq A$$
3		ledm	$$⊢{ℝ}^{*}=\mathrm{dom}\le$$
4		letsr	$$⊢\le \in \mathrm{TosetRel}$$
5	4	a1i	$$⊢\top \to \le \in \mathrm{TosetRel}$$
6	1	a1i	$$⊢\top \to A\subseteq {ℝ}^{*}$$
7	1	sseli	$$⊢x\in A\to x\in {ℝ}^{*}$$
8	1	sseli	$$⊢y\in A\to y\in {ℝ}^{*}$$
9		iccval	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left[x,y\right]=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z\le y\right)\right\}$$
10	7 8 9	syl2an	$$⊢\left(x\in A\wedge y\in A\right)\to \left[x,y\right]=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z\le y\right)\right\}$$
11	10 2	eqsstrrd	$$⊢\left(x\in A\wedge y\in A\right)\to \left\{z\in {ℝ}^{*}|\left(x\le z\wedge z\le y\right)\right\}\subseteq A$$
12	11	adantl	$$⊢\left(\top \wedge \left(x\in A\wedge y\in A\right)\right)\to \left\{z\in {ℝ}^{*}|\left(x\le z\wedge z\le y\right)\right\}\subseteq A$$
13	3 5 6 12	ordtrest2	$$⊢\top \to \mathrm{ordTop}\left(\le \cap \left(A\times A\right)\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}A$$
14	13	eqcomd	$$⊢\top \to \mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}A=\mathrm{ordTop}\left(\le \cap \left(A\times A\right)\right)$$
15	14	mptru	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}A=\mathrm{ordTop}\left(\le \cap \left(A\times A\right)\right)$$