Metamath Proof Explorer

Theorem i0oii

Description: ( 0 [,) A ) is open in II . (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Assertion i0oii ( 𝐴 ≤ 1 → ( 0 [,) 𝐴 ) ∈ II )

Proof

Step Hyp Ref Expression
1 anandi3r ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ∧ 𝑥 < 𝐴 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑥 < 𝐴 ∧ 𝐴 ≤ 1 ) ) )
2 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
3 lerelxr ⊢ ≤ ⊆ ( ℝ* × ℝ* )
4 3 brel ⊢ ( 𝐴 ≤ 1 → ( 𝐴 ∈ ℝ* ∧ 1 ∈ ℝ* ) )
5 4 simpld ⊢ ( 𝐴 ≤ 1 → 𝐴 ∈ ℝ* )
6 1xr ⊢ 1 ∈ ℝ*
7 xrltletr ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 𝑥 < 𝐴 ∧ 𝐴 ≤ 1 ) → 𝑥 < 1 ) )
8 xrltle ⊢ ( ( 𝑥 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝑥 < 1 → 𝑥 ≤ 1 ) )
9 8 3adant2 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝑥 < 1 → 𝑥 ≤ 1 ) )
10 7 9 syld ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 𝑥 < 𝐴 ∧ 𝐴 ≤ 1 ) → 𝑥 ≤ 1 ) )
11 6 10 mp3an3 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( ( 𝑥 < 𝐴 ∧ 𝐴 ≤ 1 ) → 𝑥 ≤ 1 ) )
12 2 5 11 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ) → ( ( 𝑥 < 𝐴 ∧ 𝐴 ≤ 1 ) → 𝑥 ≤ 1 ) )
13 12 imp ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑥 < 𝐴 ∧ 𝐴 ≤ 1 ) ) → 𝑥 ≤ 1 )
14 1 13 sylbi ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ∧ 𝑥 < 𝐴 ) → 𝑥 ≤ 1 )
15 14 3com12 ⊢ ( ( 𝐴 ≤ 1 ∧ 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) → 𝑥 ≤ 1 )
16 15 3expib ⊢ ( 𝐴 ≤ 1 → ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) → 𝑥 ≤ 1 ) )
17 16 pm4.71d ⊢ ( 𝐴 ≤ 1 → ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 𝑥 ≤ 1 ) ) )
18 17 anbi1d ⊢ ( 𝐴 ≤ 1 → ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 0 ≤ 𝑥 ) ↔ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 𝑥 ≤ 1 ) ∧ 0 ≤ 𝑥 ) ) )
19 3anan32 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 𝐴 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 0 ≤ 𝑥 ) )
20 3anass ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) )
21 20 anbi2i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ) )
22 anandi ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 < 𝐴 ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ) )
23 3anass ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) )
24 3anan32 ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ↔ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 𝑥 ≤ 1 ) ∧ 0 ≤ 𝑥 ) )
25 anass ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑥 < 𝐴 ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ) )
26 23 24 25 3bitr3ri ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 < 𝐴 ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ) ↔ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 𝑥 ≤ 1 ) ∧ 0 ≤ 𝑥 ) )
27 21 22 26 3bitr2i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ↔ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ 𝑥 ≤ 1 ) ∧ 0 ≤ 𝑥 ) )
28 18 19 27 3bitr4g ⊢ ( 𝐴 ≤ 1 → ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 𝐴 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ) )
29 0re ⊢ 0 ∈ ℝ
30 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 𝐴 ) ) )
31 29 5 30 sylancr ⊢ ( 𝐴 ≤ 1 → ( 𝑥 ∈ ( 0 [,) 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 𝐴 ) ) )
32 elin ⊢ ( 𝑥 ∈ ( ( -∞ (,) 𝐴 ) ∩ ( 0 [,] 1 ) ) ↔ ( 𝑥 ∈ ( -∞ (,) 𝐴 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) )
33 elicc01 ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) )
34 33 anbi2i ⊢ ( ( 𝑥 ∈ ( -∞ (,) 𝐴 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ↔ ( 𝑥 ∈ ( -∞ (,) 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) )
35 32 34 bitri ⊢ ( 𝑥 ∈ ( ( -∞ (,) 𝐴 ) ∩ ( 0 [,] 1 ) ) ↔ ( 𝑥 ∈ ( -∞ (,) 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) )
36 elioomnf ⊢ ( 𝐴 ∈ ℝ* → ( 𝑥 ∈ ( -∞ (,) 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ) )
37 5 36 syl ⊢ ( 𝐴 ≤ 1 → ( 𝑥 ∈ ( -∞ (,) 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ) )
38 37 anbi1d ⊢ ( 𝐴 ≤ 1 → ( ( 𝑥 ∈ ( -∞ (,) 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ) )
39 35 38 syl5bb ⊢ ( 𝐴 ≤ 1 → ( 𝑥 ∈ ( ( -∞ (,) 𝐴 ) ∩ ( 0 [,] 1 ) ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) ) ) )
40 28 31 39 3bitr4rd ⊢ ( 𝐴 ≤ 1 → ( 𝑥 ∈ ( ( -∞ (,) 𝐴 ) ∩ ( 0 [,] 1 ) ) ↔ 𝑥 ∈ ( 0 [,) 𝐴 ) ) )
41 40 eqrdv ⊢ ( 𝐴 ≤ 1 → ( ( -∞ (,) 𝐴 ) ∩ ( 0 [,] 1 ) ) = ( 0 [,) 𝐴 ) )
42 fvex ⊢ ( topGen ‘ ran (,) ) ∈ V
43 ovex ⊢ ( 0 [,] 1 ) ∈ V
44 iooretop ⊢ ( -∞ (,) 𝐴 ) ∈ ( topGen ‘ ran (,) )
45 elrestr ⊢ ( ( ( topGen ‘ ran (,) ) ∈ V ∧ ( 0 [,] 1 ) ∈ V ∧ ( -∞ (,) 𝐴 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( -∞ (,) 𝐴 ) ∩ ( 0 [,] 1 ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) )
46 42 43 44 45 mp3an ⊢ ( ( -∞ (,) 𝐴 ) ∩ ( 0 [,] 1 ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
47 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
48 46 47 eleqtrri ⊢ ( ( -∞ (,) 𝐴 ) ∩ ( 0 [,] 1 ) ) ∈ II
49 41 48 eqeltrrdi ⊢ ( 𝐴 ≤ 1 → ( 0 [,) 𝐴 ) ∈ II )