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 ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) )