Theorem iooii

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

	Ref	Expression
Assertion	iooii	⊢ ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) → ( 𝐴 (,) 𝐵 ) ∈ II )

Proof

Step	Hyp	Ref	Expression
1		0xr	⊢ 0 ∈ ℝ*
2		1xr	⊢ 1 ∈ ℝ*
3		ioossioo	⊢ ( ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 0 (,) 1 ) )
4	1 2 3	mpanl12	⊢ ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 0 (,) 1 ) )
5		iooretop	⊢ ( 𝐴 (,) 𝐵 ) ∈ ( 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 ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( 0 (,) 1 ) ) ) → ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 (,) 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) ) )
11	8 9 10	mpanl12	⊢ ( ( ( 0 (,) 1 ) ∈ ( topGen ‘ ran (,) ) ∧ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( 0 (,) 1 ) ) → ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 (,) 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) ) )
12	6 7 11	mp3an12	⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( 0 (,) 1 ) → ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 (,) 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) ) )
13	5 12	mpbii	⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( 0 (,) 1 ) → ( 𝐴 (,) 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) )
14		dfii2	⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
15	13 14	eleqtrrdi	⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( 0 (,) 1 ) → ( 𝐴 (,) 𝐵 ) ∈ II )
16	4 15	syl	⊢ ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 1 ) → ( 𝐴 (,) 𝐵 ) ∈ II )