Metamath Proof Explorer

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 ≤ A ∧ B ≤ 1 → A B ∈ Clsd ⁡ II

Proof

Step Hyp Ref Expression
1 iccssxr ⊢ 0 1 ⊆ ℝ *
2 iccordt ⊢ A B ∈ Clsd ⁡ ordTop ⁡ ≤
3 0re ⊢ 0 ∈ ℝ
4 1re ⊢ 1 ∈ ℝ
5 iccss ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ A ∧ B ≤ 1 → A B ⊆ 0 1
6 3 4 5 mpanl12 ⊢ 0 ≤ A ∧ B ≤ 1 → A B ⊆ 0 1
7 letopuni ⊢ ℝ * = ⋃ ordTop ⁡ ≤
8 7 restcldi ⊢ 0 1 ⊆ ℝ * ∧ A B ∈ Clsd ⁡ ordTop ⁡ ≤ ∧ A B ⊆ 0 1 → A B ∈ Clsd ⁡ ordTop ⁡ ≤ ↾ 𝑡 0 1
9 1 2 6 8 mp3an12i ⊢ 0 ≤ A ∧ B ≤ 1 → A B ∈ Clsd ⁡ ordTop ⁡ ≤ ↾ 𝑡 0 1
10 dfii5 ⊢ II = ordTop ⁡ ≤ ∩ 0 1 × 0 1
11 ordtresticc ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 1 = ordTop ⁡ ≤ ∩ 0 1 × 0 1
12 10 11 eqtr4i ⊢ II = ordTop ⁡ ≤ ↾ 𝑡 0 1
13 12 fveq2i ⊢ Clsd ⁡ II = Clsd ⁡ ordTop ⁡ ≤ ↾ 𝑡 0 1
14 9 13 eleqtrrdi ⊢ 0 ≤ A ∧ B ≤ 1 → A B ∈ Clsd ⁡ II