Step | Hyp | Ref
| Expression |
1 | | letop 21382 |
. . . . . . . 8
⊢
(ordTop‘ ≤ ) ∈ Top |
2 | | ioof 12561 |
. . . . . . . . . . 11
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
3 | | ffn 6279 |
. . . . . . . . . . 11
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . 10
⊢ (,) Fn
(ℝ* × ℝ*) |
5 | | iooordt 21393 |
. . . . . . . . . . 11
⊢ (𝑥(,)𝑦) ∈ (ordTop‘ ≤
) |
6 | 5 | rgen2w 3135 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* (𝑥(,)𝑦) ∈ (ordTop‘ ≤
) |
7 | | ffnov 7025 |
. . . . . . . . . 10
⊢
((,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) ↔ ((,) Fn
(ℝ* × ℝ*) ∧ ∀𝑥 ∈ ℝ*
∀𝑦 ∈
ℝ* (𝑥(,)𝑦) ∈ (ordTop‘ ≤
))) |
8 | 4, 6, 7 | mpbir2an 704 |
. . . . . . . . 9
⊢
(,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) |
9 | | frn 6285 |
. . . . . . . . 9
⊢
((,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) → ran (,) ⊆
(ordTop‘ ≤ )) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢ ran (,)
⊆ (ordTop‘ ≤ ) |
11 | | tgss 21144 |
. . . . . . . 8
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ran (,) ⊆ (ordTop‘
≤ )) → (topGen‘ran (,)) ⊆ (topGen‘(ordTop‘ ≤
))) |
12 | 1, 10, 11 | mp2an 685 |
. . . . . . 7
⊢
(topGen‘ran (,)) ⊆ (topGen‘(ordTop‘ ≤
)) |
13 | | tgtop 21149 |
. . . . . . . 8
⊢
((ordTop‘ ≤ ) ∈ Top → (topGen‘(ordTop‘
≤ )) = (ordTop‘ ≤ )) |
14 | 1, 13 | ax-mp 5 |
. . . . . . 7
⊢
(topGen‘(ordTop‘ ≤ )) = (ordTop‘ ≤
) |
15 | 12, 14 | sseqtri 3863 |
. . . . . 6
⊢
(topGen‘ran (,)) ⊆ (ordTop‘ ≤ ) |
16 | 15 | sseli 3824 |
. . . . 5
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ∈
(ordTop‘ ≤ )) |
17 | | retopon 22938 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
18 | | toponss 21103 |
. . . . . 6
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ 𝑥 ∈ (topGen‘ran (,)))
→ 𝑥 ⊆
ℝ) |
19 | 17, 18 | mpan 683 |
. . . . 5
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ⊆
ℝ) |
20 | | reordt 21394 |
. . . . . 6
⊢ ℝ
∈ (ordTop‘ ≤ ) |
21 | | restopn2 21353 |
. . . . . 6
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ (ordTop‘
≤ )) → (𝑥 ∈
((ordTop‘ ≤ ) ↾t ℝ) ↔ (𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑥 ⊆
ℝ))) |
22 | 1, 20, 21 | mp2an 685 |
. . . . 5
⊢ (𝑥 ∈ ((ordTop‘ ≤ )
↾t ℝ) ↔ (𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑥 ⊆
ℝ)) |
23 | 16, 19, 22 | sylanbrc 580 |
. . . 4
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ∈
((ordTop‘ ≤ ) ↾t ℝ)) |
24 | 23 | ssriv 3832 |
. . 3
⊢
(topGen‘ran (,)) ⊆ ((ordTop‘ ≤ )
↾t ℝ) |
25 | | eqid 2826 |
. . . . . . 7
⊢ ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) |
26 | | eqid 2826 |
. . . . . . 7
⊢ ran
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) = ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) |
27 | | eqid 2826 |
. . . . . . 7
⊢ ran (,) =
ran (,) |
28 | 25, 26, 27 | leordtval 21389 |
. . . . . 6
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) |
29 | 28 | oveq1i 6916 |
. . . . 5
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
((topGen‘((ran (𝑥
∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))) ↾t ℝ) |
30 | 28, 1 | eqeltrri 2904 |
. . . . . . 7
⊢
(topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top |
31 | | tgclb 21146 |
. . . . . . 7
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ↔ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top) |
32 | 30, 31 | mpbir 223 |
. . . . . 6
⊢ ((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases |
33 | | reex 10344 |
. . . . . 6
⊢ ℝ
∈ V |
34 | | tgrest 21335 |
. . . . . 6
⊢ ((((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ∧ ℝ ∈ V) → (topGen‘(((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↾t
ℝ)) = ((topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ↾t ℝ)) |
35 | 32, 33, 34 | mp2an 685 |
. . . . 5
⊢
(topGen‘(((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ↾t ℝ)) = ((topGen‘((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,))) ↾t
ℝ) |
36 | 29, 35 | eqtr4i 2853 |
. . . 4
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
(topGen‘(((ran (𝑥
∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ↾t ℝ)) |
37 | | retopbas 22935 |
. . . . 5
⊢ ran (,)
∈ TopBases |
38 | | elrest 16442 |
. . . . . . . 8
⊢ ((((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ∧ ℝ ∈ V) → (𝑢 ∈ (((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ↾t ℝ) ↔ ∃𝑣 ∈ ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))𝑢 = (𝑣 ∩
ℝ))) |
39 | 32, 33, 38 | mp2an 685 |
. . . . . . 7
⊢ (𝑢 ∈ (((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↾t
ℝ) ↔ ∃𝑣
∈ ((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))𝑢 = (𝑣 ∩ ℝ)) |
40 | | elun 3981 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↔ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∨ 𝑣 ∈ ran
(,))) |
41 | | elun 3981 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
↔ (𝑣 ∈ ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∨ 𝑣 ∈ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))) |
42 | | vex 3418 |
. . . . . . . . . . . . . . 15
⊢ 𝑣 ∈ V |
43 | | eqid 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)) =
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) |
44 | 43 | elrnmpt 5606 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞))) |
45 | 42, 44 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞)) |
46 | | simpl 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑥 ∈
ℝ*) |
47 | | pnfxr 10411 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ +∞
∈ ℝ* |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ +∞ ∈ ℝ*) |
49 | | rexr 10403 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) |
50 | 49 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 ∈
ℝ*) |
51 | | df-ioc 12469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (,] =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)}) |
52 | 51 | elixx3g 12477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (𝑥(,]+∞) ↔ ((𝑥 ∈ ℝ* ∧ +∞
∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) |
53 | 52 | baib 533 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) |
54 | 46, 48, 50, 53 | syl3anc 1496 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) |
55 | | pnfge 12251 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) |
56 | 50, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 ≤
+∞) |
57 | 56 | biantrud 529 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) |
58 | | ltpnf 12241 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → 𝑦 < +∞) |
59 | 58 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 <
+∞) |
60 | 59 | biantrud 529 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
61 | 54, 57, 60 | 3bitr2d 299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
62 | 61 | pm5.32da 576 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ ℝ
∧ 𝑦 ∈ (𝑥(,]+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝑥 < 𝑦 ∧ 𝑦 < +∞)))) |
63 | | elin 4024 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ) ↔ (𝑦 ∈ (𝑥(,]+∞) ∧ 𝑦 ∈ ℝ)) |
64 | | ancom 454 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ (𝑥(,]+∞) ∧ 𝑦 ∈ ℝ) ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ (𝑥(,]+∞))) |
65 | 63, 64 | bitri 267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ) ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ (𝑥(,]+∞))) |
66 | | 3anass 1122 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞) ↔ (𝑦 ∈ ℝ ∧ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
67 | 62, 65, 66 | 3bitr4g 306 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ)
↔ (𝑦 ∈ ℝ
∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
68 | | elioo2 12505 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑦 ∈ (𝑥(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
69 | 47, 68 | mpan2 684 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ (𝑥(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
70 | 67, 69 | bitr4d 274 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ)
↔ 𝑦 ∈ (𝑥(,)+∞))) |
71 | 70 | eqrdv 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ((𝑥(,]+∞)
∩ ℝ) = (𝑥(,)+∞)) |
72 | | ioorebas 12565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥(,)+∞) ∈ ran
(,) |
73 | 71, 72 | syl6eqel 2915 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
→ ((𝑥(,]+∞)
∩ ℝ) ∈ ran (,)) |
74 | | ineq1 4035 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑥(,]+∞) → (𝑣 ∩ ℝ) = ((𝑥(,]+∞) ∩ ℝ)) |
75 | 74 | eleq1d 2892 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝑥(,]+∞) → ((𝑣 ∩ ℝ) ∈ ran (,) ↔ ((𝑥(,]+∞) ∩ ℝ)
∈ ran (,))) |
76 | 73, 75 | syl5ibrcom 239 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ (𝑣 = (𝑥(,]+∞) → (𝑣 ∩ ℝ) ∈ ran
(,))) |
77 | 76 | rexlimiv 3237 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞) →
(𝑣 ∩ ℝ) ∈
ran (,)) |
78 | 45, 77 | sylbi 209 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) → (𝑣 ∩ ℝ) ∈ ran
(,)) |
79 | | eqid 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)) =
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) |
80 | 79 | elrnmpt 5606 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥))) |
81 | 42, 80 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥)) |
82 | | mnfxr 10415 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ -∞
∈ ℝ* |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ ∈ ℝ*) |
84 | | df-ico 12470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ [,) =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏)}) |
85 | 84 | elixx3g 12477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (-∞[,)𝑥) ↔ ((-∞ ∈
ℝ* ∧ 𝑥
∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ (-∞
≤ 𝑦 ∧ 𝑦 < 𝑥))) |
86 | 85 | baib 533 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((-∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ ≤ 𝑦 ∧
𝑦 < 𝑥))) |
87 | 83, 46, 50, 86 | syl3anc 1496 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ ≤ 𝑦 ∧
𝑦 < 𝑥))) |
88 | | mnfle 12256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ*
→ -∞ ≤ 𝑦) |
89 | 50, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ ≤ 𝑦) |
90 | 89 | biantrurd 530 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 < 𝑥 ↔ (-∞ ≤ 𝑦 ∧ 𝑦 < 𝑥))) |
91 | | mnflt 12244 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → -∞
< 𝑦) |
92 | 91 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ < 𝑦) |
93 | 92 | biantrurd 530 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 < 𝑥 ↔ (-∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
94 | 87, 90, 93 | 3bitr2d 299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ < 𝑦 ∧
𝑦 < 𝑥))) |
95 | 94 | pm5.32da 576 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ ℝ
∧ 𝑦 ∈
(-∞[,)𝑥)) ↔
(𝑦 ∈ ℝ ∧
(-∞ < 𝑦 ∧
𝑦 < 𝑥)))) |
96 | | elin 4024 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((-∞[,)𝑥) ∩ ℝ) ↔ (𝑦 ∈ (-∞[,)𝑥) ∧ 𝑦 ∈ ℝ)) |
97 | | ancom 454 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ (-∞[,)𝑥) ∧ 𝑦 ∈ ℝ) ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ (-∞[,)𝑥))) |
98 | 96, 97 | bitri 267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((-∞[,)𝑥) ∩ ℝ) ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ (-∞[,)𝑥))) |
99 | | 3anass 1122 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ -∞
< 𝑦 ∧ 𝑦 < 𝑥) ↔ (𝑦 ∈ ℝ ∧ (-∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
100 | 95, 98, 99 | 3bitr4g 306 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
((-∞[,)𝑥) ∩
ℝ) ↔ (𝑦 ∈
ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
101 | | elioo2 12505 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((-∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ*) → (𝑦 ∈ (-∞(,)𝑥) ↔ (𝑦 ∈ ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
102 | 82, 101 | mpan 683 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
(-∞(,)𝑥) ↔
(𝑦 ∈ ℝ ∧
-∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
103 | 100, 102 | bitr4d 274 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
((-∞[,)𝑥) ∩
ℝ) ↔ 𝑦 ∈
(-∞(,)𝑥))) |
104 | 103 | eqrdv 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ((-∞[,)𝑥)
∩ ℝ) = (-∞(,)𝑥)) |
105 | | ioorebas 12565 |
. . . . . . . . . . . . . . . . 17
⊢
(-∞(,)𝑥)
∈ ran (,) |
106 | 104, 105 | syl6eqel 2915 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
→ ((-∞[,)𝑥)
∩ ℝ) ∈ ran (,)) |
107 | | ineq1 4035 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (-∞[,)𝑥) → (𝑣 ∩ ℝ) = ((-∞[,)𝑥) ∩
ℝ)) |
108 | 107 | eleq1d 2892 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (-∞[,)𝑥) → ((𝑣 ∩ ℝ) ∈ ran (,) ↔
((-∞[,)𝑥) ∩
ℝ) ∈ ran (,))) |
109 | 106, 108 | syl5ibrcom 239 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ (𝑣 =
(-∞[,)𝑥) →
(𝑣 ∩ ℝ) ∈
ran (,))) |
110 | 109 | rexlimiv 3237 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥) →
(𝑣 ∩ ℝ) ∈
ran (,)) |
111 | 81, 110 | sylbi 209 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) →
(𝑣 ∩ ℝ) ∈
ran (,)) |
112 | 78, 111 | jaoi 890 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∨ 𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) →
(𝑣 ∩ ℝ) ∈
ran (,)) |
113 | 41, 112 | sylbi 209 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
→ (𝑣 ∩ ℝ)
∈ ran (,)) |
114 | | elssuni 4690 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,)) |
115 | | unirnioo 12563 |
. . . . . . . . . . . . . 14
⊢ ℝ =
∪ ran (,) |
116 | 114, 115 | syl6sseqr 3878 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆
ℝ) |
117 | | df-ss 3813 |
. . . . . . . . . . . . 13
⊢ (𝑣 ⊆ ℝ ↔ (𝑣 ∩ ℝ) = 𝑣) |
118 | 116, 117 | sylib 210 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ran (,) → (𝑣 ∩ ℝ) = 𝑣) |
119 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ ran
(,)) |
120 | 118, 119 | eqeltrd 2907 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ran (,) → (𝑣 ∩ ℝ) ∈ ran
(,)) |
121 | 113, 120 | jaoi 890 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∨ 𝑣 ∈ ran (,))
→ (𝑣 ∩ ℝ)
∈ ran (,)) |
122 | 40, 121 | sylbi 209 |
. . . . . . . . 9
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) → (𝑣 ∩ ℝ) ∈ ran
(,)) |
123 | | eleq1 2895 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∩ ℝ) → (𝑢 ∈ ran (,) ↔ (𝑣 ∩ ℝ) ∈ ran
(,))) |
124 | 122, 123 | syl5ibrcom 239 |
. . . . . . . 8
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) → (𝑢 = (𝑣 ∩ ℝ) → 𝑢 ∈ ran (,))) |
125 | 124 | rexlimiv 3237 |
. . . . . . 7
⊢
(∃𝑣 ∈
((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))𝑢 = (𝑣 ∩ ℝ) → 𝑢 ∈ ran (,)) |
126 | 39, 125 | sylbi 209 |
. . . . . 6
⊢ (𝑢 ∈ (((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↾t
ℝ) → 𝑢 ∈
ran (,)) |
127 | 126 | ssriv 3832 |
. . . . 5
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ↾t ℝ) ⊆ ran (,) |
128 | | tgss 21144 |
. . . . 5
⊢ ((ran (,)
∈ TopBases ∧ (((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ↾t ℝ) ⊆ ran (,)) →
(topGen‘(((ran (𝑥
∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ↾t ℝ)) ⊆ (topGen‘ran
(,))) |
129 | 37, 127, 128 | mp2an 685 |
. . . 4
⊢
(topGen‘(((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ↾t ℝ)) ⊆ (topGen‘ran
(,)) |
130 | 36, 129 | eqsstri 3861 |
. . 3
⊢
((ordTop‘ ≤ ) ↾t ℝ) ⊆
(topGen‘ran (,)) |
131 | 24, 130 | eqssi 3844 |
. 2
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) |
132 | | xrtgioo.1 |
. 2
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t ℝ) |
133 | 131, 132 | eqtr4i 2853 |
1
⊢
(topGen‘ran (,)) = 𝐽 |