| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0xr 11308 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ* | 
| 2 |  | lerelxr 11324 | . . . . . . . . . . . . 13
⊢  ≤
⊆ (ℝ* × ℝ*) | 
| 3 | 2 | brel 5750 | . . . . . . . . . . . 12
⊢ (0 ≤
𝐴 → (0 ∈
ℝ* ∧ 𝐴
∈ ℝ*)) | 
| 4 | 3 | simprd 495 | . . . . . . . . . . 11
⊢ (0 ≤
𝐴 → 𝐴 ∈
ℝ*) | 
| 5 |  | rexr 11307 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) | 
| 6 |  | xrlelttr 13198 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ*)
→ ((0 ≤ 𝐴 ∧
𝐴 < 𝑥) → 0 < 𝑥)) | 
| 7 |  | xrltle 13191 | . . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ 𝑥 ∈ ℝ*) → (0 <
𝑥 → 0 ≤ 𝑥)) | 
| 8 | 7 | 3adant2 1132 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ*)
→ (0 < 𝑥 → 0
≤ 𝑥)) | 
| 9 | 6, 8 | syld 47 | . . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ*)
→ ((0 ≤ 𝐴 ∧
𝐴 < 𝑥) → 0 ≤ 𝑥)) | 
| 10 | 1, 4, 5, 9 | mp3an3an 1469 | . . . . . . . . . 10
⊢ ((0 ≤
𝐴 ∧ 𝑥 ∈ ℝ) → ((0 ≤ 𝐴 ∧ 𝐴 < 𝑥) → 0 ≤ 𝑥)) | 
| 11 | 10 | imp 406 | . . . . . . . . 9
⊢ (((0 ≤
𝐴 ∧ 𝑥 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝑥)) → 0 ≤ 𝑥) | 
| 12 | 11 | 3impdi 1351 | . . . . . . . 8
⊢ ((0 ≤
𝐴 ∧ 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 0 ≤ 𝑥) | 
| 13 | 12 | 3expib 1123 | . . . . . . 7
⊢ (0 ≤
𝐴 → ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 0 ≤ 𝑥)) | 
| 14 | 13 | pm4.71d 561 | . . . . . 6
⊢ (0 ≤
𝐴 → ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 0 ≤ 𝑥))) | 
| 15 | 14 | anbi1d 631 | . . . . 5
⊢ (0 ≤
𝐴 → (((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 ≤ 1) ↔ (((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 0 ≤ 𝑥) ∧ 𝑥 ≤ 1))) | 
| 16 |  | df-3an 1089 | . . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 1) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 ≤ 1)) | 
| 17 |  | 3anass 1095 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1) ↔ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) | 
| 18 | 17 | anbi2i 623 | . . . . . 6
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 19 |  | anandi 676 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝐴 < 𝑥 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (𝑥 ∈ ℝ ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 20 |  | anass 468 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 0 ≤ 𝑥) ∧ 𝑥 ≤ 1) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) | 
| 21 |  | anass 468 | . . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 < 𝑥 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 22 | 20, 21 | bitr2i 276 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝐴 < 𝑥 ∧ (0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) ↔ (((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 0 ≤ 𝑥) ∧ 𝑥 ≤ 1)) | 
| 23 | 18, 19, 22 | 3bitr2i 299 | . . . . 5
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ (((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 0 ≤ 𝑥) ∧ 𝑥 ≤ 1)) | 
| 24 | 15, 16, 23 | 3bitr4g 314 | . . . 4
⊢ (0 ≤
𝐴 → ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 1) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 25 |  | 1re 11261 | . . . . 5
⊢ 1 ∈
ℝ | 
| 26 |  | elioc2 13450 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 1 ∈ ℝ) → (𝑥 ∈ (𝐴(,]1) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 1))) | 
| 27 | 4, 25, 26 | sylancl 586 | . . . 4
⊢ (0 ≤
𝐴 → (𝑥 ∈ (𝐴(,]1) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 1))) | 
| 28 |  | elin 3967 | . . . . . 6
⊢ (𝑥 ∈ ((𝐴(,)+∞) ∩ (0[,]1)) ↔ (𝑥 ∈ (𝐴(,)+∞) ∧ 𝑥 ∈ (0[,]1))) | 
| 29 |  | elicc01 13506 | . . . . . . 7
⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1)) | 
| 30 | 29 | anbi2i 623 | . . . . . 6
⊢ ((𝑥 ∈ (𝐴(,)+∞) ∧ 𝑥 ∈ (0[,]1)) ↔ (𝑥 ∈ (𝐴(,)+∞) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) | 
| 31 | 28, 30 | bitri 275 | . . . . 5
⊢ (𝑥 ∈ ((𝐴(,)+∞) ∩ (0[,]1)) ↔ (𝑥 ∈ (𝐴(,)+∞) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))) | 
| 32 |  | elioopnf 13483 | . . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥))) | 
| 33 | 4, 32 | syl 17 | . . . . . 6
⊢ (0 ≤
𝐴 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥))) | 
| 34 | 33 | anbi1d 631 | . . . . 5
⊢ (0 ≤
𝐴 → ((𝑥 ∈ (𝐴(,)+∞) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 35 | 31, 34 | bitrid 283 | . . . 4
⊢ (0 ≤
𝐴 → (𝑥 ∈ ((𝐴(,)+∞) ∩ (0[,]1)) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1)))) | 
| 36 | 24, 27, 35 | 3bitr4rd 312 | . . 3
⊢ (0 ≤
𝐴 → (𝑥 ∈ ((𝐴(,)+∞) ∩ (0[,]1)) ↔ 𝑥 ∈ (𝐴(,]1))) | 
| 37 | 36 | eqrdv 2735 | . 2
⊢ (0 ≤
𝐴 → ((𝐴(,)+∞) ∩ (0[,]1)) =
(𝐴(,]1)) | 
| 38 |  | fvex 6919 | . . . 4
⊢
(topGen‘ran (,)) ∈ V | 
| 39 |  | ovex 7464 | . . . 4
⊢ (0[,]1)
∈ V | 
| 40 |  | iooretop 24786 | . . . 4
⊢ (𝐴(,)+∞) ∈
(topGen‘ran (,)) | 
| 41 |  | elrestr 17473 | . . . 4
⊢
(((topGen‘ran (,)) ∈ V ∧ (0[,]1) ∈ V ∧ (𝐴(,)+∞) ∈
(topGen‘ran (,))) → ((𝐴(,)+∞) ∩ (0[,]1)) ∈
((topGen‘ran (,)) ↾t (0[,]1))) | 
| 42 | 38, 39, 40, 41 | mp3an 1463 | . . 3
⊢ ((𝐴(,)+∞) ∩ (0[,]1))
∈ ((topGen‘ran (,)) ↾t (0[,]1)) | 
| 43 |  | dfii2 24908 | . . 3
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) | 
| 44 | 42, 43 | eleqtrri 2840 | . 2
⊢ ((𝐴(,)+∞) ∩ (0[,]1))
∈ II | 
| 45 | 37, 44 | eqeltrrdi 2850 | 1
⊢ (0 ≤
𝐴 → (𝐴(,]1) ∈ II) |