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	⊢ 𝐴 ⊆ ℝ*
	ordtrestixx.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
Assertion	ordtrestixx	⊢ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) = ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordtrestixx.1	⊢ 𝐴 ⊆ ℝ*
2		ordtrestixx.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
3		ledm	⊢ ℝ* = dom ≤
4		letsr	⊢ ≤ ∈ TosetRel
5	4	a1i	⊢ ( ⊤ → ≤ ∈ TosetRel )
6	1	a1i	⊢ ( ⊤ → 𝐴 ⊆ ℝ* )
7	1	sseli	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℝ* )
8	1	sseli	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ* )
9		iccval	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 [,] 𝑦 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
10	7 8 9	syl2an	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 [,] 𝑦 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
11	10 2	eqsstrrd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ⊆ 𝐴 )
12	11	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ⊆ 𝐴 )
13	3 5 6 12	ordtrest2	⊢ ( ⊤ → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
14	13	eqcomd	⊢ ( ⊤ → ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) = ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
15	14	mptru	⊢ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) = ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) )