Metamath Proof Explorer

Theorem iccordt

Description: A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion iccordt ⊢ A B ∈ Clsd ⁡ ordTop ⁡ ≤

Proof

Step Hyp Ref Expression
1 df-ov ⊢ A B = . ⁡ A B
2 letsr ⊢ ≤ ∈ TosetRel
3 ledm ⊢ ℝ * = dom ⁡ ≤
4 3 ordtcld3 ⊢ ≤ ∈ TosetRel ∧ x ∈ ℝ * ∧ y ∈ ℝ * → z ∈ ℝ * | x ≤ z ∧ z ≤ y ∈ Clsd ⁡ ordTop ⁡ ≤
5 2 4 mp3an1 ⊢ x ∈ ℝ * ∧ y ∈ ℝ * → z ∈ ℝ * | x ≤ z ∧ z ≤ y ∈ Clsd ⁡ ordTop ⁡ ≤
6 5 rgen2 ⊢ ∀ x ∈ ℝ * ∀ y ∈ ℝ * z ∈ ℝ * | x ≤ z ∧ z ≤ y ∈ Clsd ⁡ ordTop ⁡ ≤
7 df-icc ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x ≤ z ∧ z ≤ y
8 7 fmpo ⊢ ∀ x ∈ ℝ * ∀ y ∈ ℝ * z ∈ ℝ * | x ≤ z ∧ z ≤ y ∈ Clsd ⁡ ordTop ⁡ ≤ ↔ . : ℝ * × ℝ * ⟶ Clsd ⁡ ordTop ⁡ ≤
9 6 8 mpbi ⊢ . : ℝ * × ℝ * ⟶ Clsd ⁡ ordTop ⁡ ≤
10 letop ⊢ ordTop ⁡ ≤ ∈ Top
11 0cld ⊢ ordTop ⁡ ≤ ∈ Top → ∅ ∈ Clsd ⁡ ordTop ⁡ ≤
12 10 11 ax-mp ⊢ ∅ ∈ Clsd ⁡ ordTop ⁡ ≤
13 9 12 f0cli ⊢ . ⁡ A B ∈ Clsd ⁡ ordTop ⁡ ≤
14 1 13 eqeltri ⊢ A B ∈ Clsd ⁡ ordTop ⁡ ≤