Theorem ordtresticc

Description: The restriction of the less than order to a closed interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Assertion	ordtresticc	⊢ ( ( ordTop ‘ ≤ ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccssxr	⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ*
2		iccss2	⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 ) )
3	1 2	ordtrestixx	⊢ ( ( ordTop ‘ ≤ ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )