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

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