This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⁡ ≤ ↾ 𝑡 A B = ordTop ⁡ ≤ ∩ A B × A B

Proof

Step Hyp Ref Expression
1 iccssxr ⊢ A B ⊆ ℝ *
2 iccss2 ⊢ x ∈ A B ∧ y ∈ A B → x y ⊆ A B
3 1 2 ordtrestixx ⊢ ordTop ⁡ ≤ ↾ 𝑡 A B = ordTop ⁡ ≤ ∩ A B × A B