Theorem icccldii

Description: Closed intervals are closed sets of II . Note that iccss , iccordt , and ordtresticc are proved from ixxss12 , ordtcld3 , and ordtrest2 , respectively. An alternate proof uses restcldi , dfii2 , and icccld . (Contributed by Zhi Wang, 8-Sep-2024)

	Ref	Expression
Assertion	icccldii	⊢ ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ II ) )

Proof

Step	Hyp	Ref	Expression
1		iccssxr	⊢ ( 0 [,] 1 ) ⊆ ℝ*
2		iccordt	⊢ ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) )
3		0re	⊢ 0 ∈ ℝ
4		1re	⊢ 1 ∈ ℝ
5		iccss	⊢ ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 0 [,] 1 ) )
6	3 4 5	mpanl12	⊢ ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 0 [,] 1 ) )
7		letopuni	⊢ ℝ* = ∪ ( ordTop ‘ ≤ )
8	7	restcldi	⊢ ( ( ( 0 [,] 1 ) ⊆ ℝ* ∧ ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ordTop ‘ ≤ ) ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ( 0 [,] 1 ) ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) ) )
9	1 2 6 8	mp3an12i	⊢ ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) ) )
10		dfii5	⊢ II = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
11		ordtresticc	⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) = ( ordTop ‘ ( ≤ ∩ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
12	10 11	eqtr4i	⊢ II = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) )
13	12	fveq2i	⊢ ( Clsd ‘ II ) = ( Clsd ‘ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] 1 ) ) )
14	9 13	eleqtrrdi	⊢ ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ II ) )