Step | Hyp | Ref
| Expression |
1 | | anandi3r 1104 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ∧ 𝑥 < 𝐴) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1) ∧ (𝑥 < 𝐴 ∧ 𝐴 ≤ 1))) |
2 | | rexr 10765 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
3 | | lerelxr 10782 |
. . . . . . . . . . . . . 14
⊢ ≤
⊆ (ℝ* × ℝ*) |
4 | 3 | brel 5588 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≤ 1 → (𝐴 ∈ ℝ*
∧ 1 ∈ ℝ*)) |
5 | 4 | simpld 498 |
. . . . . . . . . . . 12
⊢ (𝐴 ≤ 1 → 𝐴 ∈
ℝ*) |
6 | | 1xr 10778 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ* |
7 | | xrltletr 12633 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ* ∧ 1 ∈ ℝ*) → ((𝑥 < 𝐴 ∧ 𝐴 ≤ 1) → 𝑥 < 1)) |
8 | | xrltle 12625 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 1 ∈ ℝ*) → (𝑥 < 1 → 𝑥 ≤ 1)) |
9 | 8 | 3adant2 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ* ∧ 1 ∈ ℝ*) → (𝑥 < 1 → 𝑥 ≤ 1)) |
10 | 7, 9 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ* ∧ 1 ∈ ℝ*) → ((𝑥 < 𝐴 ∧ 𝐴 ≤ 1) → 𝑥 ≤ 1)) |
11 | 6, 10 | mp3an3 1451 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → ((𝑥 < 𝐴 ∧ 𝐴 ≤ 1) → 𝑥 ≤ 1)) |
12 | 2, 5, 11 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1) → ((𝑥 < 𝐴 ∧ 𝐴 ≤ 1) → 𝑥 ≤ 1)) |
13 | 12 | imp 410 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1) ∧ (𝑥 < 𝐴 ∧ 𝐴 ≤ 1)) → 𝑥 ≤ 1) |
14 | 1, 13 | sylbi 220 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ∧ 𝑥 < 𝐴) → 𝑥 ≤ 1) |
15 | 14 | 3com12 1124 |
. . . . . . . 8
⊢ ((𝐴 ≤ 1 ∧ 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) → 𝑥 ≤ 1) |
16 | 15 | 3expib 1123 |
. . . . . . 7
⊢ (𝐴 ≤ 1 → ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) → 𝑥 ≤ 1)) |
17 | 16 | pm4.71d 565 |
. . . . . 6
⊢ (𝐴 ≤ 1 → ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1))) |
18 | 17 | anbi1d 633 |
. . . . 5
⊢ (𝐴 ≤ 1 → (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 0 ≤ 𝑥) ↔ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1) ∧ 0 ≤ 𝑥))) |
19 | | 3anan32 1098 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 < 𝐴) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 0 ≤ 𝑥)) |
20 | | 3anass 1096 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1) ↔ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) |
21 | 20 | anbi2i 626 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) |
22 | | anandi 676 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 < 𝐴 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) |
23 | | 3anass 1096 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) |
24 | | 3anan32 1098 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1) ↔ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1) ∧ 0 ≤ 𝑥)) |
25 | | anass 472 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ (𝑥 ∈ ℝ ∧ (𝑥 < 𝐴 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) |
26 | 23, 24, 25 | 3bitr3ri 305 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 < 𝐴 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) ↔ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1) ∧ 0 ≤ 𝑥)) |
27 | 21, 22, 26 | 3bitr2i 302 |
. . . . 5
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1) ∧ 0 ≤ 𝑥)) |
28 | 18, 19, 27 | 3bitr4g 317 |
. . . 4
⊢ (𝐴 ≤ 1 → ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 < 𝐴) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) |
29 | | 0re 10721 |
. . . . 5
⊢ 0 ∈
ℝ |
30 | | elico2 12885 |
. . . . 5
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ*) → (𝑥 ∈ (0[,)𝐴) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 𝐴))) |
31 | 29, 5, 30 | sylancr 590 |
. . . 4
⊢ (𝐴 ≤ 1 → (𝑥 ∈ (0[,)𝐴) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 𝐴))) |
32 | | elin 3859 |
. . . . . 6
⊢ (𝑥 ∈ ((-∞(,)𝐴) ∩ (0[,]1)) ↔ (𝑥 ∈ (-∞(,)𝐴) ∧ 𝑥 ∈ (0[,]1))) |
33 | | elicc01 12940 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1)) |
34 | 33 | anbi2i 626 |
. . . . . 6
⊢ ((𝑥 ∈ (-∞(,)𝐴) ∧ 𝑥 ∈ (0[,]1)) ↔ (𝑥 ∈ (-∞(,)𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) |
35 | 32, 34 | bitri 278 |
. . . . 5
⊢ (𝑥 ∈ ((-∞(,)𝐴) ∩ (0[,]1)) ↔ (𝑥 ∈ (-∞(,)𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) |
36 | | elioomnf 12918 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈
(-∞(,)𝐴) ↔
(𝑥 ∈ ℝ ∧
𝑥 < 𝐴))) |
37 | 5, 36 | syl 17 |
. . . . . 6
⊢ (𝐴 ≤ 1 → (𝑥 ∈ (-∞(,)𝐴) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝐴))) |
38 | 37 | anbi1d 633 |
. . . . 5
⊢ (𝐴 ≤ 1 → ((𝑥 ∈ (-∞(,)𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) |
39 | 35, 38 | syl5bb 286 |
. . . 4
⊢ (𝐴 ≤ 1 → (𝑥 ∈ ((-∞(,)𝐴) ∩ (0[,]1)) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) |
40 | 28, 31, 39 | 3bitr4rd 315 |
. . 3
⊢ (𝐴 ≤ 1 → (𝑥 ∈ ((-∞(,)𝐴) ∩ (0[,]1)) ↔ 𝑥 ∈ (0[,)𝐴))) |
41 | 40 | eqrdv 2736 |
. 2
⊢ (𝐴 ≤ 1 →
((-∞(,)𝐴) ∩
(0[,]1)) = (0[,)𝐴)) |
42 | | fvex 6687 |
. . . 4
⊢
(topGen‘ran (,)) ∈ V |
43 | | ovex 7203 |
. . . 4
⊢ (0[,]1)
∈ V |
44 | | iooretop 23518 |
. . . 4
⊢
(-∞(,)𝐴)
∈ (topGen‘ran (,)) |
45 | | elrestr 16805 |
. . . 4
⊢
(((topGen‘ran (,)) ∈ V ∧ (0[,]1) ∈ V ∧
(-∞(,)𝐴) ∈
(topGen‘ran (,))) → ((-∞(,)𝐴) ∩ (0[,]1)) ∈ ((topGen‘ran
(,)) ↾t (0[,]1))) |
46 | 42, 43, 44, 45 | mp3an 1462 |
. . 3
⊢
((-∞(,)𝐴)
∩ (0[,]1)) ∈ ((topGen‘ran (,)) ↾t
(0[,]1)) |
47 | | dfii2 23634 |
. . 3
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
48 | 46, 47 | eleqtrri 2832 |
. 2
⊢
((-∞(,)𝐴)
∩ (0[,]1)) ∈ II |
49 | 41, 48 | eqeltrrdi 2842 |
1
⊢ (𝐴 ≤ 1 → (0[,)𝐴) ∈ II) |