Metamath Proof Explorer

Theorem i0oii

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

Ref Expression
Assertion i0oii ⊢ A ≤ 1 → 0 A ∈ II

Proof

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