Metamath Proof Explorer

Theorem io1ii

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

Ref Expression
Assertion io1ii ( 0 ≤ 𝐴 → ( 𝐴 (,] 1 ) ∈ II )

Proof

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