| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | anandi3r 1103 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ∧ 𝑥 < 𝐴) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1) ∧ (𝑥 < 𝐴 ∧ 𝐴 ≤ 1))) | 
| 2 |  | rexr 11307 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) | 
| 3 |  | lerelxr 11324 | . . . . . . . . . . . . . 14
⊢  ≤
⊆ (ℝ* × ℝ*) | 
| 4 | 3 | brel 5750 | . . . . . . . . . . . . 13
⊢ (𝐴 ≤ 1 → (𝐴 ∈ ℝ*
∧ 1 ∈ ℝ*)) | 
| 5 | 4 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝐴 ≤ 1 → 𝐴 ∈
ℝ*) | 
| 6 |  | 1xr 11320 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ* | 
| 7 |  | xrltletr 13199 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ* ∧ 1 ∈ ℝ*) → ((𝑥 < 𝐴 ∧ 𝐴 ≤ 1) → 𝑥 < 1)) | 
| 8 |  | xrltle 13191 | . . . . . . . . . . . . . . 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 1452 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → ((𝑥 < 𝐴 ∧ 𝐴 ≤ 1) → 𝑥 ≤ 1)) | 
| 12 | 2, 5, 11 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1) → ((𝑥 < 𝐴 ∧ 𝐴 ≤ 1) → 𝑥 ≤ 1)) | 
| 13 | 12 | imp 406 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1) ∧ (𝑥 < 𝐴 ∧ 𝐴 ≤ 1)) → 𝑥 ≤ 1) | 
| 14 | 1, 13 | sylbi 217 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ≤ 1 ∧ 𝑥 < 𝐴) → 𝑥 ≤ 1) | 
| 15 | 14 | 3com12 1124 | . . . . . . . 8
⊢ ((𝐴 ≤ 1 ∧ 𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) → 𝑥 ≤ 1) | 
| 16 | 15 | 3expib 1123 | . . . . . . 7
⊢ (𝐴 ≤ 1 → ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) → 𝑥 ≤ 1)) | 
| 17 | 16 | pm4.71d 561 | . . . . . 6
⊢ (𝐴 ≤ 1 → ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1))) | 
| 18 | 17 | anbi1d 631 | . . . . 5
⊢ (𝐴 ≤ 1 → (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 0 ≤ 𝑥) ↔ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1) ∧ 0 ≤ 𝑥))) | 
| 19 |  | 3anan32 1097 | . . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 < 𝐴) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 0 ≤ 𝑥)) | 
| 20 |  | 3anass 1095 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1) ↔ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) | 
| 21 | 20 | anbi2i 623 | . . . . . 6
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 22 |  | anandi 676 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 < 𝐴 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 23 |  | 3anass 1095 | . . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) | 
| 24 |  | 3anan32 1097 | . . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1) ↔ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1) ∧ 0 ≤ 𝑥)) | 
| 25 |  | anass 468 | . . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ (𝑥 ∈ ℝ ∧ (𝑥 < 𝐴 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 26 | 23, 24, 25 | 3bitr3ri 302 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 < 𝐴 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) ↔ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1) ∧ 0 ≤ 𝑥)) | 
| 27 | 21, 22, 26 | 3bitr2i 299 | . . . . 5
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ (((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ 𝑥 ≤ 1) ∧ 0 ≤ 𝑥)) | 
| 28 | 18, 19, 27 | 3bitr4g 314 | . . . 4
⊢ (𝐴 ≤ 1 → ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 < 𝐴) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 29 |  | 0re 11263 | . . . . 5
⊢ 0 ∈
ℝ | 
| 30 |  | elico2 13451 | . . . . 5
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ*) → (𝑥 ∈ (0[,)𝐴) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 𝐴))) | 
| 31 | 29, 5, 30 | sylancr 587 | . . . 4
⊢ (𝐴 ≤ 1 → (𝑥 ∈ (0[,)𝐴) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 𝐴))) | 
| 32 |  | elin 3967 | . . . . . 6
⊢ (𝑥 ∈ ((-∞(,)𝐴) ∩ (0[,]1)) ↔ (𝑥 ∈ (-∞(,)𝐴) ∧ 𝑥 ∈ (0[,]1))) | 
| 33 |  | elicc01 13506 | . . . . . . 7
⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1)) | 
| 34 | 33 | anbi2i 623 | . . . . . 6
⊢ ((𝑥 ∈ (-∞(,)𝐴) ∧ 𝑥 ∈ (0[,]1)) ↔ (𝑥 ∈ (-∞(,)𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) | 
| 35 | 32, 34 | bitri 275 | . . . . 5
⊢ (𝑥 ∈ ((-∞(,)𝐴) ∩ (0[,]1)) ↔ (𝑥 ∈ (-∞(,)𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) | 
| 36 |  | elioomnf 13484 | . . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈
(-∞(,)𝐴) ↔
(𝑥 ∈ ℝ ∧
𝑥 < 𝐴))) | 
| 37 | 5, 36 | syl 17 | . . . . . 6
⊢ (𝐴 ≤ 1 → (𝑥 ∈ (-∞(,)𝐴) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 𝐴))) | 
| 38 | 37 | anbi1d 631 | . . . . 5
⊢ (𝐴 ≤ 1 → ((𝑥 ∈ (-∞(,)𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 39 | 35, 38 | bitrid 283 | . . . 4
⊢ (𝐴 ≤ 1 → (𝑥 ∈ ((-∞(,)𝐴) ∩ (0[,]1)) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 < 𝐴) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 40 | 28, 31, 39 | 3bitr4rd 312 | . . 3
⊢ (𝐴 ≤ 1 → (𝑥 ∈ ((-∞(,)𝐴) ∩ (0[,]1)) ↔ 𝑥 ∈ (0[,)𝐴))) | 
| 41 | 40 | eqrdv 2735 | . 2
⊢ (𝐴 ≤ 1 →
((-∞(,)𝐴) ∩
(0[,]1)) = (0[,)𝐴)) | 
| 42 |  | fvex 6919 | . . . 4
⊢
(topGen‘ran (,)) ∈ V | 
| 43 |  | ovex 7464 | . . . 4
⊢ (0[,]1)
∈ V | 
| 44 |  | iooretop 24786 | . . . 4
⊢
(-∞(,)𝐴)
∈ (topGen‘ran (,)) | 
| 45 |  | elrestr 17473 | . . . 4
⊢
(((topGen‘ran (,)) ∈ V ∧ (0[,]1) ∈ V ∧
(-∞(,)𝐴) ∈
(topGen‘ran (,))) → ((-∞(,)𝐴) ∩ (0[,]1)) ∈ ((topGen‘ran
(,)) ↾t (0[,]1))) | 
| 46 | 42, 43, 44, 45 | mp3an 1463 | . . 3
⊢
((-∞(,)𝐴)
∩ (0[,]1)) ∈ ((topGen‘ran (,)) ↾t
(0[,]1)) | 
| 47 |  | dfii2 24908 | . . 3
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) | 
| 48 | 46, 47 | eleqtrri 2840 | . 2
⊢
((-∞(,)𝐴)
∩ (0[,]1)) ∈ II | 
| 49 | 41, 48 | eqeltrrdi 2850 | 1
⊢ (𝐴 ≤ 1 → (0[,)𝐴) ∈ II) |