Step | Hyp | Ref
| Expression |
1 | | letop 22103 |
. . . . . . . 8
⊢
(ordTop‘ ≤ ) ∈ Top |
2 | | ioof 13035 |
. . . . . . . . . . 11
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
3 | | ffn 6545 |
. . . . . . . . . . 11
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . 10
⊢ (,) Fn
(ℝ* × ℝ*) |
5 | | iooordt 22114 |
. . . . . . . . . . 11
⊢ (𝑥(,)𝑦) ∈ (ordTop‘ ≤
) |
6 | 5 | rgen2w 3074 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* (𝑥(,)𝑦) ∈ (ordTop‘ ≤
) |
7 | | ffnov 7337 |
. . . . . . . . . 10
⊢
((,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) ↔ ((,) Fn
(ℝ* × ℝ*) ∧ ∀𝑥 ∈ ℝ*
∀𝑦 ∈
ℝ* (𝑥(,)𝑦) ∈ (ordTop‘ ≤
))) |
8 | 4, 6, 7 | mpbir2an 711 |
. . . . . . . . 9
⊢
(,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) |
9 | | frn 6552 |
. . . . . . . . 9
⊢
((,):(ℝ* ×
ℝ*)⟶(ordTop‘ ≤ ) → ran (,) ⊆
(ordTop‘ ≤ )) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢ ran (,)
⊆ (ordTop‘ ≤ ) |
11 | | tgss 21865 |
. . . . . . . 8
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ran (,) ⊆ (ordTop‘
≤ )) → (topGen‘ran (,)) ⊆ (topGen‘(ordTop‘ ≤
))) |
12 | 1, 10, 11 | mp2an 692 |
. . . . . . 7
⊢
(topGen‘ran (,)) ⊆ (topGen‘(ordTop‘ ≤
)) |
13 | | tgtop 21870 |
. . . . . . . 8
⊢
((ordTop‘ ≤ ) ∈ Top → (topGen‘(ordTop‘
≤ )) = (ordTop‘ ≤ )) |
14 | 1, 13 | ax-mp 5 |
. . . . . . 7
⊢
(topGen‘(ordTop‘ ≤ )) = (ordTop‘ ≤
) |
15 | 12, 14 | sseqtri 3937 |
. . . . . 6
⊢
(topGen‘ran (,)) ⊆ (ordTop‘ ≤ ) |
16 | 15 | sseli 3896 |
. . . . 5
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ∈
(ordTop‘ ≤ )) |
17 | | retopon 23661 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
18 | | toponss 21824 |
. . . . . 6
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ 𝑥 ∈ (topGen‘ran (,)))
→ 𝑥 ⊆
ℝ) |
19 | 17, 18 | mpan 690 |
. . . . 5
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ⊆
ℝ) |
20 | | reordt 22115 |
. . . . . 6
⊢ ℝ
∈ (ordTop‘ ≤ ) |
21 | | restopn2 22074 |
. . . . . 6
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ (ordTop‘
≤ )) → (𝑥 ∈
((ordTop‘ ≤ ) ↾t ℝ) ↔ (𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑥 ⊆
ℝ))) |
22 | 1, 20, 21 | mp2an 692 |
. . . . 5
⊢ (𝑥 ∈ ((ordTop‘ ≤ )
↾t ℝ) ↔ (𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑥 ⊆
ℝ)) |
23 | 16, 19, 22 | sylanbrc 586 |
. . . 4
⊢ (𝑥 ∈ (topGen‘ran (,))
→ 𝑥 ∈
((ordTop‘ ≤ ) ↾t ℝ)) |
24 | 23 | ssriv 3905 |
. . 3
⊢
(topGen‘ran (,)) ⊆ ((ordTop‘ ≤ )
↾t ℝ) |
25 | | eqid 2737 |
. . . . . . 7
⊢ ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) |
26 | | eqid 2737 |
. . . . . . 7
⊢ ran
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) = ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) |
27 | | eqid 2737 |
. . . . . . 7
⊢ ran (,) =
ran (,) |
28 | 25, 26, 27 | leordtval 22110 |
. . . . . 6
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) |
29 | 28 | oveq1i 7223 |
. . . . 5
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
((topGen‘((ran (𝑥
∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))) ↾t ℝ) |
30 | 28, 1 | eqeltrri 2835 |
. . . . . . 7
⊢
(topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top |
31 | | tgclb 21867 |
. . . . . . 7
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ↔ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top) |
32 | 30, 31 | mpbir 234 |
. . . . . 6
⊢ ((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases |
33 | | reex 10820 |
. . . . . 6
⊢ ℝ
∈ V |
34 | | tgrest 22056 |
. . . . . 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 2768 |
. . . 4
⊢
((ordTop‘ ≤ ) ↾t ℝ) =
(topGen‘(((ran (𝑥
∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ↾t ℝ)) |
37 | | retopbas 23658 |
. . . . 5
⊢ ran (,)
∈ TopBases |
38 | | elrest 16932 |
. . . . . . . 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 4063 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↔ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∨ 𝑣 ∈ ran
(,))) |
41 | | elun 4063 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
↔ (𝑣 ∈ ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∨ 𝑣 ∈ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))) |
42 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)) =
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) |
43 | 42 | elrnmpt 5825 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞))) |
44 | 43 | elv 3414 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞)) |
45 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑥 ∈
ℝ*) |
46 | | pnfxr 10887 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ +∞
∈ ℝ* |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ +∞ ∈ ℝ*) |
48 | | rexr 10879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) |
49 | 48 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 ∈
ℝ*) |
50 | | df-ioc 12940 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (,] =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)}) |
51 | 50 | elixx3g 12948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (𝑥(,]+∞) ↔ ((𝑥 ∈ ℝ* ∧ +∞
∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) |
52 | 51 | baib 539 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) |
53 | 45, 47, 49, 52 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) |
54 | | pnfge 12722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) |
55 | 49, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 ≤
+∞) |
56 | 55 | biantrud 535 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∧ 𝑦 ≤ +∞))) |
57 | | ltpnf 12712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → 𝑦 < +∞) |
58 | 57 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ 𝑦 <
+∞) |
59 | 58 | biantrud 535 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
60 | 53, 56, 59 | 3bitr2d 310 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈ (𝑥(,]+∞) ↔ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
61 | 60 | pm5.32da 582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ ℝ
∧ 𝑦 ∈ (𝑥(,]+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝑥 < 𝑦 ∧ 𝑦 < +∞)))) |
62 | | elin 3882 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ) ↔ (𝑦 ∈ (𝑥(,]+∞) ∧ 𝑦 ∈ ℝ)) |
63 | 62 | biancomi 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ) ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ (𝑥(,]+∞))) |
64 | | 3anass 1097 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞) ↔ (𝑦 ∈ ℝ ∧ (𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
65 | 61, 63, 64 | 3bitr4g 317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ)
↔ (𝑦 ∈ ℝ
∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
66 | | elioo2 12976 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑦 ∈ (𝑥(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
67 | 46, 66 | mpan2 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ (𝑥(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞))) |
68 | 65, 67 | bitr4d 285 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ ((𝑥(,]+∞) ∩ ℝ)
↔ 𝑦 ∈ (𝑥(,)+∞))) |
69 | 68 | eqrdv 2735 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ((𝑥(,]+∞)
∩ ℝ) = (𝑥(,)+∞)) |
70 | | ioorebas 13039 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥(,)+∞) ∈ ran
(,) |
71 | 69, 70 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
→ ((𝑥(,]+∞)
∩ ℝ) ∈ ran (,)) |
72 | | ineq1 4120 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑥(,]+∞) → (𝑣 ∩ ℝ) = ((𝑥(,]+∞) ∩ ℝ)) |
73 | 72 | eleq1d 2822 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝑥(,]+∞) → ((𝑣 ∩ ℝ) ∈ ran (,) ↔ ((𝑥(,]+∞) ∩ ℝ)
∈ ran (,))) |
74 | 71, 73 | syl5ibrcom 250 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ (𝑣 = (𝑥(,]+∞) → (𝑣 ∩ ℝ) ∈ ran
(,))) |
75 | 74 | rexlimiv 3199 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℝ* 𝑣 =
(𝑥(,]+∞) →
(𝑣 ∩ ℝ) ∈
ran (,)) |
76 | 44, 75 | sylbi 220 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) → (𝑣 ∩ ℝ) ∈ ran
(,)) |
77 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)) =
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) |
78 | 77 | elrnmpt 5825 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥))) |
79 | 78 | elv 3414 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ↔
∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥)) |
80 | | mnfxr 10890 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ -∞
∈ ℝ* |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ ∈ ℝ*) |
82 | | df-ico 12941 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ [,) =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏)}) |
83 | 82 | elixx3g 12948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (-∞[,)𝑥) ↔ ((-∞ ∈
ℝ* ∧ 𝑥
∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ (-∞
≤ 𝑦 ∧ 𝑦 < 𝑥))) |
84 | 83 | baib 539 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((-∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ ≤ 𝑦 ∧
𝑦 < 𝑥))) |
85 | 81, 45, 49, 84 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ ≤ 𝑦 ∧
𝑦 < 𝑥))) |
86 | | mnfle 12726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ*
→ -∞ ≤ 𝑦) |
87 | 49, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ ≤ 𝑦) |
88 | 87 | biantrurd 536 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 < 𝑥 ↔ (-∞ ≤ 𝑦 ∧ 𝑦 < 𝑥))) |
89 | | mnflt 12715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → -∞
< 𝑦) |
90 | 89 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ -∞ < 𝑦) |
91 | 90 | biantrurd 536 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 < 𝑥 ↔ (-∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
92 | 85, 88, 91 | 3bitr2d 310 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈ ℝ)
→ (𝑦 ∈
(-∞[,)𝑥) ↔
(-∞ < 𝑦 ∧
𝑦 < 𝑥))) |
93 | 92 | pm5.32da 582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ ℝ
∧ 𝑦 ∈
(-∞[,)𝑥)) ↔
(𝑦 ∈ ℝ ∧
(-∞ < 𝑦 ∧
𝑦 < 𝑥)))) |
94 | | elin 3882 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((-∞[,)𝑥) ∩ ℝ) ↔ (𝑦 ∈ (-∞[,)𝑥) ∧ 𝑦 ∈ ℝ)) |
95 | 94 | biancomi 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((-∞[,)𝑥) ∩ ℝ) ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ (-∞[,)𝑥))) |
96 | | 3anass 1097 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ -∞
< 𝑦 ∧ 𝑦 < 𝑥) ↔ (𝑦 ∈ ℝ ∧ (-∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
97 | 93, 95, 96 | 3bitr4g 317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
((-∞[,)𝑥) ∩
ℝ) ↔ (𝑦 ∈
ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
98 | | elioo2 12976 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((-∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ*) → (𝑦 ∈ (-∞(,)𝑥) ↔ (𝑦 ∈ ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
99 | 80, 98 | mpan 690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
(-∞(,)𝑥) ↔
(𝑦 ∈ ℝ ∧
-∞ < 𝑦 ∧ 𝑦 < 𝑥))) |
100 | 97, 99 | bitr4d 285 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈
((-∞[,)𝑥) ∩
ℝ) ↔ 𝑦 ∈
(-∞(,)𝑥))) |
101 | 100 | eqrdv 2735 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ((-∞[,)𝑥)
∩ ℝ) = (-∞(,)𝑥)) |
102 | | ioorebas 13039 |
. . . . . . . . . . . . . . . . 17
⊢
(-∞(,)𝑥)
∈ ran (,) |
103 | 101, 102 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
→ ((-∞[,)𝑥)
∩ ℝ) ∈ ran (,)) |
104 | | ineq1 4120 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (-∞[,)𝑥) → (𝑣 ∩ ℝ) = ((-∞[,)𝑥) ∩
ℝ)) |
105 | 104 | eleq1d 2822 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (-∞[,)𝑥) → ((𝑣 ∩ ℝ) ∈ ran (,) ↔
((-∞[,)𝑥) ∩
ℝ) ∈ ran (,))) |
106 | 103, 105 | syl5ibrcom 250 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ (𝑣 =
(-∞[,)𝑥) →
(𝑣 ∩ ℝ) ∈
ran (,))) |
107 | 106 | rexlimiv 3199 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℝ* 𝑣 =
(-∞[,)𝑥) →
(𝑣 ∩ ℝ) ∈
ran (,)) |
108 | 79, 107 | sylbi 220 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) →
(𝑣 ∩ ℝ) ∈
ran (,)) |
109 | 76, 108 | jaoi 857 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∨ 𝑣 ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) →
(𝑣 ∩ ℝ) ∈
ran (,)) |
110 | 41, 109 | sylbi 220 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
→ (𝑣 ∩ ℝ)
∈ ran (,)) |
111 | | elssuni 4851 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,)) |
112 | | unirnioo 13037 |
. . . . . . . . . . . . . 14
⊢ ℝ =
∪ ran (,) |
113 | 111, 112 | sseqtrrdi 3952 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆
ℝ) |
114 | | df-ss 3883 |
. . . . . . . . . . . . 13
⊢ (𝑣 ⊆ ℝ ↔ (𝑣 ∩ ℝ) = 𝑣) |
115 | 113, 114 | sylib 221 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ran (,) → (𝑣 ∩ ℝ) = 𝑣) |
116 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ ran
(,)) |
117 | 115, 116 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ran (,) → (𝑣 ∩ ℝ) ∈ ran
(,)) |
118 | 110, 117 | jaoi 857 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∨ 𝑣 ∈ ran (,))
→ (𝑣 ∩ ℝ)
∈ ran (,)) |
119 | 40, 118 | sylbi 220 |
. . . . . . . . 9
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) → (𝑣 ∩ ℝ) ∈ ran
(,)) |
120 | | eleq1 2825 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∩ ℝ) → (𝑢 ∈ ran (,) ↔ (𝑣 ∩ ℝ) ∈ ran
(,))) |
121 | 119, 120 | syl5ibrcom 250 |
. . . . . . . 8
⊢ (𝑣 ∈ ((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) → (𝑢 = (𝑣 ∩ ℝ) → 𝑢 ∈ ran (,))) |
122 | 121 | rexlimiv 3199 |
. . . . . . 7
⊢
(∃𝑣 ∈
((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))𝑢 = (𝑣 ∩ ℝ) → 𝑢 ∈ ran (,)) |
123 | 39, 122 | sylbi 220 |
. . . . . 6
⊢ (𝑢 ∈ (((ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ↾t
ℝ) → 𝑢 ∈
ran (,)) |
124 | 123 | ssriv 3905 |
. . . . 5
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ↾t ℝ) ⊆ ran (,) |
125 | | tgss 21865 |
. . . . 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 3935 |
. . 3
⊢
((ordTop‘ ≤ ) ↾t ℝ) ⊆
(topGen‘ran (,)) |
128 | 24, 127 | eqssi 3917 |
. 2
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) |
129 | | xrtgioo.1 |
. 2
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t ℝ) |
130 | 128, 129 | eqtr4i 2768 |
1
⊢
(topGen‘ran (,)) = 𝐽 |