| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | letop 23215 | . . . . . . . 8
⊢
(ordTop‘ ≤ ) ∈ Top | 
| 2 |  | ioof 13488 | . . . . . . . . . . 11
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ | 
| 3 |  | ffn 6735 | . . . . . . . . . . 11
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) | 
| 4 | 2, 3 | ax-mp 5 | . . . . . . . . . 10
⊢ (,) Fn
(ℝ* × ℝ*) | 
| 5 |  | iooordt 23226 | . . . . . . . . . . 11
⊢ (𝑥(,)𝑦) ∈ (ordTop‘ ≤
) | 
| 6 | 5 | rgen2w 3065 | . . . . . . . . . 10
⊢
∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* (𝑥(,)𝑦) ∈ (ordTop‘ ≤
) | 
| 7 |  | ffnov 7560 | . . . . . . . . . 10
⊢
((,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) ↔ ((,) Fn
(ℝ* × ℝ*) ∧ ∀𝑥 ∈ ℝ*
∀𝑦 ∈
ℝ* (𝑥(,)𝑦) ∈ (ordTop‘ ≤
))) | 
| 8 | 4, 6, 7 | mpbir2an 711 | . . . . . . . . 9
⊢
(,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) | 
| 9 |  | frn 6742 | . . . . . . . . 9
⊢
((,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) → ran (,) ⊆
(ordTop‘ ≤ )) | 
| 10 | 8, 9 | ax-mp 5 | . . . . . . . 8
⊢ ran (,)
⊆ (ordTop‘ ≤ ) | 
| 11 |  | tgss 22976 | . . . . . . . 8
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ran (,) ⊆ (ordTop‘
≤ )) → (topGen‘ran (,)) ⊆ (topGen‘(ordTop‘ ≤
))) | 
| 12 | 1, 10, 11 | mp2an 692 | . . . . . . 7
⊢
(topGen‘ran (,)) ⊆ (topGen‘(ordTop‘ ≤
)) | 
| 13 |  | tgtop 22981 | . . . . . . . 8
⊢
((ordTop‘ ≤ ) ∈ Top → (topGen‘(ordTop‘
≤ )) = (ordTop‘ ≤ )) | 
| 14 | 1, 13 | ax-mp 5 | . . . . . . 7
⊢
(topGen‘(ordTop‘ ≤ )) = (ordTop‘ ≤
) | 
| 15 | 12, 14 | sseqtri 4031 | . . . . . 6
⊢
(topGen‘ran (,)) ⊆ (ordTop‘ ≤ ) | 
| 16 | 15 | sseli 3978 | . . . . 5
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ∈
(ordTop‘ ≤ )) | 
| 17 |  | retopon 24785 | . . . . . 6
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) | 
| 18 |  | toponss 22934 | . . . . . 6
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ 𝑥 ∈ (topGen‘ran (,)))
→ 𝑥 ⊆
ℝ) | 
| 19 | 17, 18 | mpan 690 | . . . . 5
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ⊆
ℝ) | 
| 20 |  | reordt 23227 | . . . . . 6
⊢ ℝ
∈ (ordTop‘ ≤ ) | 
| 21 |  | restopn2 23186 | . . . . . 6
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ (ordTop‘
≤ )) → (𝑥 ∈
((ordTop‘ ≤ ) ↾t ℝ) ↔ (𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑥 ⊆
ℝ))) | 
| 22 | 1, 20, 21 | mp2an 692 | . . . . 5
⊢ (𝑥 ∈ ((ordTop‘ ≤ )
↾t ℝ) ↔ (𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑥 ⊆
ℝ)) | 
| 23 | 16, 19, 22 | sylanbrc 583 | . . . 4
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ∈
((ordTop‘ ≤ ) ↾t ℝ)) | 
| 24 | 23 | ssriv 3986 | . . 3
⊢
(topGen‘ran (,)) ⊆ ((ordTop‘ ≤ )
↾t ℝ) | 
| 25 |  | eqid 2736 | . . . . . . 7
⊢ ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) | 
| 26 |  | eqid 2736 | . . . . . . 7
⊢ ran
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) = ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) | 
| 27 |  | eqid 2736 | . . . . . . 7
⊢ ran (,) =
ran (,) | 
| 28 | 25, 26, 27 | leordtval 23222 | . . . . . 6
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) | 
| 29 | 28 | oveq1i 7442 | . . . . 5
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
((topGen‘((ran (𝑥
∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))) ↾t ℝ) | 
| 30 | 28, 1 | eqeltrri 2837 | . . . . . . 7
⊢
(topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top | 
| 31 |  | tgclb 22978 | . . . . . . 7
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ↔ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top) | 
| 32 | 30, 31 | mpbir 231 | . . . . . 6
⊢ ((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases | 
| 33 |  | reex 11247 | . . . . . 6
⊢ ℝ
∈ V | 
| 34 |  | tgrest 23168 | . . . . . 6
⊢ ((((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ∧ ℝ ∈ V) → (topGen‘(((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↾t
ℝ)) = ((topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ↾t ℝ)) | 
| 35 | 32, 33, 34 | mp2an 692 | . . . . 5
⊢
(topGen‘(((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ↾t ℝ)) = ((topGen‘((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,))) ↾t
ℝ) | 
| 36 | 29, 35 | eqtr4i 2767 | . . . 4
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
(topGen‘(((ran (𝑥
∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ↾t ℝ)) | 
| 37 |  | retopbas 24782 | . . . . 5
⊢ ran (,)
∈ TopBases | 
| 38 |  | elrest 17473 | . . . . . . . 8
⊢ ((((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ∧ ℝ ∈ V) → (𝑢 ∈ (((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ↾t ℝ) ↔ ∃𝑣 ∈ ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))𝑢 = (𝑣 ∩
ℝ))) | 
| 39 | 32, 33, 38 | mp2an 692 | . . . . . . 7
⊢ (𝑢 ∈ (((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↾t
ℝ) ↔ ∃𝑣
∈ ((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))𝑢 = (𝑣 ∩ ℝ)) | 
| 40 |  | elun 4152 | . . . . . . . . . 10
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↔ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∨ 𝑣 ∈ ran
(,))) | 
| 41 |  | elun 4152 | . . . . . . . . . . . 12
⊢ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
↔ (𝑣 ∈ ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∨ 𝑣 ∈ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))) | 
| 42 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)) =
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) | 
| 43 | 42 | elrnmpt 5968 | . . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞))) | 
| 44 | 43 | elv 3484 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞)) | 
| 45 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑥 ∈
ℝ*) | 
| 46 |  | pnfxr 11316 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ +∞
∈ ℝ* | 
| 47 | 46 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ +∞ ∈ ℝ*) | 
| 48 |  | rexr 11308 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) | 
| 49 | 48 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 ∈
ℝ*) | 
| 50 |  | df-ioc 13393 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (,] =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)}) | 
| 51 | 50 | elixx3g 13401 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (𝑥(,]+∞) ↔ ((𝑥 ∈ ℝ* ∧ +∞
∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) | 
| 52 | 51 | baib 535 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) | 
| 53 | 45, 47, 49, 52 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) | 
| 54 |  | pnfge 13173 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) | 
| 55 | 49, 54 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 ≤
+∞) | 
| 56 | 55 | biantrud 531 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) | 
| 57 |  | ltpnf 13163 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → 𝑦 < +∞) | 
| 58 | 57 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 <
+∞) | 
| 59 | 58 | biantrud 531 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) | 
| 60 | 53, 56, 59 | 3bitr2d 307 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) | 
| 61 | 60 | pm5.32da 579 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ ℝ
∧ 𝑦 ∈ (𝑥(,]+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝑥 < 𝑦 ∧ 𝑦 < +∞)))) | 
| 62 |  | elin 3966 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ) ↔ (𝑦 ∈ (𝑥(,]+∞) ∧ 𝑦 ∈ ℝ)) | 
| 63 | 62 | biancomi 462 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ) ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ (𝑥(,]+∞))) | 
| 64 |  | 3anass 1094 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞) ↔ (𝑦 ∈ ℝ ∧ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) | 
| 65 | 61, 63, 64 | 3bitr4g 314 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ)
↔ (𝑦 ∈ ℝ
∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) | 
| 66 |  | elioo2 13429 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑦 ∈ (𝑥(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) | 
| 67 | 46, 66 | mpan2 691 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ (𝑥(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) | 
| 68 | 65, 67 | bitr4d 282 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ)
↔ 𝑦 ∈ (𝑥(,)+∞))) | 
| 69 | 68 | eqrdv 2734 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ((𝑥(,]+∞)
∩ ℝ) = (𝑥(,)+∞)) | 
| 70 |  | ioorebas 13492 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥(,)+∞) ∈ ran
(,) | 
| 71 | 69, 70 | eqeltrdi 2848 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
→ ((𝑥(,]+∞)
∩ ℝ) ∈ ran (,)) | 
| 72 |  | ineq1 4212 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑥(,]+∞) → (𝑣 ∩ ℝ) = ((𝑥(,]+∞) ∩ ℝ)) | 
| 73 | 72 | eleq1d 2825 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝑥(,]+∞) → ((𝑣 ∩ ℝ) ∈ ran (,) ↔ ((𝑥(,]+∞) ∩ ℝ)
∈ ran (,))) | 
| 74 | 71, 73 | syl5ibrcom 247 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ (𝑣 = (𝑥(,]+∞) → (𝑣 ∩ ℝ) ∈ ran
(,))) | 
| 75 | 74 | rexlimiv 3147 | . . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞) →
(𝑣 ∩ ℝ) ∈
ran (,)) | 
| 76 | 44, 75 | sylbi 217 | . . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) → (𝑣 ∩ ℝ) ∈ ran
(,)) | 
| 77 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)) =
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) | 
| 78 | 77 | elrnmpt 5968 | . . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥))) | 
| 79 | 78 | elv 3484 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥)) | 
| 80 |  | mnfxr 11319 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ -∞
∈ ℝ* | 
| 81 | 80 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ ∈ ℝ*) | 
| 82 |  | df-ico 13394 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ [,) =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏)}) | 
| 83 | 82 | elixx3g 13401 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (-∞[,)𝑥) ↔ ((-∞ ∈
ℝ* ∧ 𝑥
∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ (-∞
≤ 𝑦 ∧ 𝑦 < 𝑥))) | 
| 84 | 83 | baib 535 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((-∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ ≤ 𝑦 ∧
𝑦 < 𝑥))) | 
| 85 | 81, 45, 49, 84 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ ≤ 𝑦 ∧
𝑦 < 𝑥))) | 
| 86 |  | mnfle 13178 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ*
→ -∞ ≤ 𝑦) | 
| 87 | 49, 86 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ ≤ 𝑦) | 
| 88 | 87 | biantrurd 532 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 < 𝑥 ↔ (-∞ ≤ 𝑦 ∧ 𝑦 < 𝑥))) | 
| 89 |  | mnflt 13166 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → -∞
< 𝑦) | 
| 90 | 89 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ < 𝑦) | 
| 91 | 90 | biantrurd 532 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 < 𝑥 ↔ (-∞ < 𝑦 ∧ 𝑦 < 𝑥))) | 
| 92 | 85, 88, 91 | 3bitr2d 307 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ < 𝑦 ∧
𝑦 < 𝑥))) | 
| 93 | 92 | pm5.32da 579 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ ℝ
∧ 𝑦 ∈
(-∞[,)𝑥)) ↔
(𝑦 ∈ ℝ ∧
(-∞ < 𝑦 ∧
𝑦 < 𝑥)))) | 
| 94 |  | elin 3966 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((-∞[,)𝑥) ∩ ℝ) ↔ (𝑦 ∈ (-∞[,)𝑥) ∧ 𝑦 ∈ ℝ)) | 
| 95 | 94 | biancomi 462 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((-∞[,)𝑥) ∩ ℝ) ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ (-∞[,)𝑥))) | 
| 96 |  | 3anass 1094 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ -∞
< 𝑦 ∧ 𝑦 < 𝑥) ↔ (𝑦 ∈ ℝ ∧ (-∞ < 𝑦 ∧ 𝑦 < 𝑥))) | 
| 97 | 93, 95, 96 | 3bitr4g 314 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
((-∞[,)𝑥) ∩
ℝ) ↔ (𝑦 ∈
ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥))) | 
| 98 |  | elioo2 13429 | . . . . . . . . . . . . . . . . . . . 20
⊢
((-∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ*) → (𝑦 ∈ (-∞(,)𝑥) ↔ (𝑦 ∈ ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥))) | 
| 99 | 80, 98 | mpan 690 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
(-∞(,)𝑥) ↔
(𝑦 ∈ ℝ ∧
-∞ < 𝑦 ∧ 𝑦 < 𝑥))) | 
| 100 | 97, 99 | bitr4d 282 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
((-∞[,)𝑥) ∩
ℝ) ↔ 𝑦 ∈
(-∞(,)𝑥))) | 
| 101 | 100 | eqrdv 2734 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ((-∞[,)𝑥)
∩ ℝ) = (-∞(,)𝑥)) | 
| 102 |  | ioorebas 13492 | . . . . . . . . . . . . . . . . 17
⊢
(-∞(,)𝑥)
∈ ran (,) | 
| 103 | 101, 102 | eqeltrdi 2848 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
→ ((-∞[,)𝑥)
∩ ℝ) ∈ ran (,)) | 
| 104 |  | ineq1 4212 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (-∞[,)𝑥) → (𝑣 ∩ ℝ) = ((-∞[,)𝑥) ∩
ℝ)) | 
| 105 | 104 | eleq1d 2825 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = (-∞[,)𝑥) → ((𝑣 ∩ ℝ) ∈ ran (,) ↔
((-∞[,)𝑥) ∩
ℝ) ∈ ran (,))) | 
| 106 | 103, 105 | syl5ibrcom 247 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ (𝑣 =
(-∞[,)𝑥) →
(𝑣 ∩ ℝ) ∈
ran (,))) | 
| 107 | 106 | rexlimiv 3147 | . . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥) →
(𝑣 ∩ ℝ) ∈
ran (,)) | 
| 108 | 79, 107 | sylbi 217 | . . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) →
(𝑣 ∩ ℝ) ∈
ran (,)) | 
| 109 | 76, 108 | jaoi 857 | . . . . . . . . . . . 12
⊢ ((𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∨ 𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) →
(𝑣 ∩ ℝ) ∈
ran (,)) | 
| 110 | 41, 109 | sylbi 217 | . . . . . . . . . . 11
⊢ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
→ (𝑣 ∩ ℝ)
∈ ran (,)) | 
| 111 |  | elssuni 4936 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,)) | 
| 112 |  | unirnioo 13490 | . . . . . . . . . . . . . 14
⊢ ℝ =
∪ ran (,) | 
| 113 | 111, 112 | sseqtrrdi 4024 | . . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆
ℝ) | 
| 114 |  | dfss2 3968 | . . . . . . . . . . . . 13
⊢ (𝑣 ⊆ ℝ ↔ (𝑣 ∩ ℝ) = 𝑣) | 
| 115 | 113, 114 | sylib 218 | . . . . . . . . . . . 12
⊢ (𝑣 ∈ ran (,) → (𝑣 ∩ ℝ) = 𝑣) | 
| 116 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ ran
(,)) | 
| 117 | 115, 116 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (𝑣 ∈ ran (,) → (𝑣 ∩ ℝ) ∈ ran
(,)) | 
| 118 | 110, 117 | jaoi 857 | . . . . . . . . . 10
⊢ ((𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∨ 𝑣 ∈ ran (,))
→ (𝑣 ∩ ℝ)
∈ ran (,)) | 
| 119 | 40, 118 | sylbi 217 | . . . . . . . . 9
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) → (𝑣 ∩ ℝ) ∈ ran
(,)) | 
| 120 |  | eleq1 2828 | . . . . . . . . 9
⊢ (𝑢 = (𝑣 ∩ ℝ) → (𝑢 ∈ ran (,) ↔ (𝑣 ∩ ℝ) ∈ ran
(,))) | 
| 121 | 119, 120 | syl5ibrcom 247 | . . . . . . . 8
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) → (𝑢 = (𝑣 ∩ ℝ) → 𝑢 ∈ ran (,))) | 
| 122 | 121 | rexlimiv 3147 | . . . . . . 7
⊢
(∃𝑣 ∈
((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))𝑢 = (𝑣 ∩ ℝ) → 𝑢 ∈ ran (,)) | 
| 123 | 39, 122 | sylbi 217 | . . . . . 6
⊢ (𝑢 ∈ (((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↾t
ℝ) → 𝑢 ∈
ran (,)) | 
| 124 | 123 | ssriv 3986 | . . . . 5
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ↾t ℝ) ⊆ ran (,) | 
| 125 |  | tgss 22976 | . . . . 5
⊢ ((ran (,)
∈ TopBases ∧ (((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ↾t ℝ) ⊆ ran (,)) →
(topGen‘(((ran (𝑥
∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ↾t ℝ)) ⊆ (topGen‘ran
(,))) | 
| 126 | 37, 124, 125 | mp2an 692 | . . . 4
⊢
(topGen‘(((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ↾t ℝ)) ⊆ (topGen‘ran
(,)) | 
| 127 | 36, 126 | eqsstri 4029 | . . 3
⊢
((ordTop‘ ≤ ) ↾t ℝ) ⊆
(topGen‘ran (,)) | 
| 128 | 24, 127 | eqssi 3999 | . 2
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) | 
| 129 |  | xrtgioo.1 | . 2
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t ℝ) | 
| 130 | 128, 129 | eqtr4i 2767 | 1
⊢
(topGen‘ran (,)) = 𝐽 |