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 ‘ ≤ ) )