Metamath Proof Explorer

Theorem iooii

Description: Open intervals are open sets of II . (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Assertion iooii ⊢ 0 ≤ A ∧ B ≤ 1 → A B ∈ II

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ *
2 1xr ⊢ 1 ∈ ℝ *
3 ioossioo ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ 0 ≤ A ∧ B ≤ 1 → A B ⊆ 0 1
4 1 2 3 mpanl12 ⊢ 0 ≤ A ∧ B ≤ 1 → A B ⊆ 0 1
5 iooretop ⊢ A B ∈ topGen ⁡ ran ⁡ .
6 iooretop ⊢ 0 1 ∈ topGen ⁡ ran ⁡ .
7 ioossicc ⊢ 0 1 ⊆ 0 1
8 retop ⊢ topGen ⁡ ran ⁡ . ∈ Top
9 ovex ⊢ 0 1 ∈ V
10 restopnb ⊢ topGen ⁡ ran ⁡ . ∈ Top ∧ 0 1 ∈ V ∧ 0 1 ∈ topGen ⁡ ran ⁡ . ∧ 0 1 ⊆ 0 1 ∧ A B ⊆ 0 1 → A B ∈ topGen ⁡ ran ⁡ . ↔ A B ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
11 8 9 10 mpanl12 ⊢ 0 1 ∈ topGen ⁡ ran ⁡ . ∧ 0 1 ⊆ 0 1 ∧ A B ⊆ 0 1 → A B ∈ topGen ⁡ ran ⁡ . ↔ A B ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
12 6 7 11 mp3an12 ⊢ A B ⊆ 0 1 → A B ∈ topGen ⁡ ran ⁡ . ↔ A B ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
13 5 12 mpbii ⊢ A B ⊆ 0 1 → A B ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
14 dfii2 ⊢ II = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
15 13 14 eleqtrrdi ⊢ A B ⊆ 0 1 → A B ∈ II
16 4 15 syl ⊢ 0 ≤ A ∧ B ≤ 1 → A B ∈ II