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

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 ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) )

Proof

Step Hyp Ref Expression
1 df-ov ⊢ ( 𝐴 [,] 𝐵 ) = ( [,] ‘ ⟨ 𝐴 , 𝐵 ⟩ )
2 letsr ⊢ ≤ ∈ TosetRel
3 ledm ⊢ ℝ* = dom ≤
4 3 ordtcld3 ⊢ ( ( ≤ ∈ TosetRel ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) ) )
5 2 4 mp3an1 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) ) )
6 5 rgen2 ⊢ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) )
7 df-icc ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
8 7 fmpo ⊢ ( ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ∈ ( 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 ⊢ ( [,] ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) )
14 1 13 eqeltri ⊢ ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) )