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