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 ⊢ 𝐴 ⊆ ℝ*
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 ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) )