Step | Hyp | Ref
| Expression |
1 | | sxbrsiga.0 |
. . . 4
⊢ 𝐽 = (topGen‘ran
(,)) |
2 | | dya2ioc.1 |
. . . 4
⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
3 | | dya2ioc.2 |
. . . 4
⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) |
4 | 1, 2, 3 | dya2iocucvr 29673 |
. . 3
⊢ ∪ ran 𝑅 = (ℝ ×
ℝ) |
5 | | sxbrsigalem0 29660 |
. . 3
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) = (ℝ ×
ℝ) |
6 | 4, 5 | eqtr4i 2635 |
. 2
⊢ ∪ ran 𝑅 = ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))) |
7 | | vex 3176 |
. . . . . 6
⊢ 𝑢 ∈ V |
8 | | vex 3176 |
. . . . . 6
⊢ 𝑣 ∈ V |
9 | 7, 8 | xpex 6860 |
. . . . 5
⊢ (𝑢 × 𝑣) ∈ V |
10 | 3, 9 | elrnmpt2 6671 |
. . . 4
⊢ (𝑑 ∈ ran 𝑅 ↔ ∃𝑢 ∈ ran 𝐼∃𝑣 ∈ ran 𝐼 𝑑 = (𝑢 × 𝑣)) |
11 | | simpr 476 |
. . . . . . 7
⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → 𝑑 = (𝑢 × 𝑣)) |
12 | 1, 2 | dya2icobrsiga 29665 |
. . . . . . . . . . . . 13
⊢ ran 𝐼 ⊆
𝔅ℝ |
13 | | brsigasspwrn 29575 |
. . . . . . . . . . . . 13
⊢
𝔅ℝ ⊆ 𝒫 ℝ |
14 | 12, 13 | sstri 3577 |
. . . . . . . . . . . 12
⊢ ran 𝐼 ⊆ 𝒫
ℝ |
15 | 14 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ran 𝐼 → 𝑢 ∈ 𝒫 ℝ) |
16 | 15 | elpwid 4118 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ran 𝐼 → 𝑢 ⊆ ℝ) |
17 | 14 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ran 𝐼 → 𝑣 ∈ 𝒫 ℝ) |
18 | 17 | elpwid 4118 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ran 𝐼 → 𝑣 ⊆ ℝ) |
19 | | xpinpreima2 29281 |
. . . . . . . . . 10
⊢ ((𝑢 ⊆ ℝ ∧ 𝑣 ⊆ ℝ) → (𝑢 × 𝑣) = ((◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) ∩
(◡(2nd ↾ (ℝ
× ℝ)) “ 𝑣))) |
20 | 16, 18, 19 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (𝑢 × 𝑣) = ((◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) ∩
(◡(2nd ↾ (ℝ
× ℝ)) “ 𝑣))) |
21 | | reex 9906 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
∈ V |
22 | 21 | mptex 6390 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∈ V |
23 | 22 | rnex 6992 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∈ V |
24 | 21 | mptex 6390 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞)))
∈ V |
25 | 24 | rnex 6992 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ∈ V |
26 | 23, 25 | unex 6854 |
. . . . . . . . . . . . . 14
⊢ (ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V |
27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) ∈ V) |
28 | 27 | sgsiga 29532 |
. . . . . . . . . . . 12
⊢ (⊤
→ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra) |
29 | 28 | trud 1484 |
. . . . . . . . . . 11
⊢
(sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra) |
31 | | 1stpreima 28867 |
. . . . . . . . . . . . 13
⊢ (𝑢 ⊆ ℝ → (◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) =
(𝑢 ×
ℝ)) |
32 | 16, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ran 𝐼 → (◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) =
(𝑢 ×
ℝ)) |
33 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈ V |
34 | 2, 33 | elrnmpt2 6671 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ran 𝐼 ↔ ∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
35 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
36 | 35 | xpeq1d 5062 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (𝑢 × ℝ) = (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ)) |
37 | | difxp1 5478 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞)) × ℝ) = ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∖
((((𝑥 + 1) / (2↑𝑛))[,)+∞) ×
ℝ)) |
38 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ∈
ℤ) |
39 | 38 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ∈
ℝ) |
40 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℝ+ |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 2 ∈
ℝ+) |
42 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑛 ∈
ℤ) |
43 | 41, 42 | rpexpcld 12894 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(2↑𝑛) ∈
ℝ+) |
44 | 39, 43 | rerpdivcld 11779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ∈ ℝ) |
45 | 44 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ∈
ℝ*) |
46 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 1 ∈
ℝ) |
47 | 39, 46 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 + 1) ∈
ℝ) |
48 | 47, 43 | rerpdivcld 11779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ∈
ℝ) |
49 | 48 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ∈
ℝ*) |
50 | | pnfxr 9971 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ +∞
∈ ℝ* |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → +∞
∈ ℝ*) |
52 | 39 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ≤ (𝑥 + 1)) |
53 | 39, 47, 43, 52 | lediv1dd 11806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ≤ ((𝑥 + 1) / (2↑𝑛))) |
54 | | pnfge 11840 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 + 1) / (2↑𝑛)) ∈ ℝ*
→ ((𝑥 + 1) /
(2↑𝑛)) ≤
+∞) |
55 | 49, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ≤
+∞) |
56 | | difico 28935 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 / (2↑𝑛)) ∈ ℝ* ∧ ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ ((𝑥 / (2↑𝑛)) ≤ ((𝑥 + 1) / (2↑𝑛)) ∧ ((𝑥 + 1) / (2↑𝑛)) ≤ +∞)) → (((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
57 | 45, 49, 51, 53, 55, 56 | syl32anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
58 | 57 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞)) × ℝ)
= (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ)) |
59 | 37, 58 | syl5reqr 2659 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ) = ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∖
((((𝑥 + 1) / (2↑𝑛))[,)+∞) ×
ℝ))) |
60 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra) |
61 | | ssun1 3738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ⊆ (ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) |
62 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) = (((𝑥 / (2↑𝑛))[,)+∞) ×
ℝ) |
63 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑒 = (𝑥 / (2↑𝑛)) → (𝑒[,)+∞) = ((𝑥 / (2↑𝑛))[,)+∞)) |
64 | 63 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑒 = (𝑥 / (2↑𝑛)) → ((𝑒[,)+∞) × ℝ) = (((𝑥 / (2↑𝑛))[,)+∞) ×
ℝ)) |
65 | 64 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 = (𝑥 / (2↑𝑛)) → ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) × ℝ)
↔ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ)
= (((𝑥 / (2↑𝑛))[,)+∞) ×
ℝ))) |
66 | 65 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 / (2↑𝑛)) ∈ ℝ ∧ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) = (((𝑥 / (2↑𝑛))[,)+∞) × ℝ)) →
∃𝑒 ∈ ℝ
(((𝑥 / (2↑𝑛))[,)+∞) × ℝ)
= ((𝑒[,)+∞) ×
ℝ)) |
67 | 44, 62, 66 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
∃𝑒 ∈ ℝ
(((𝑥 / (2↑𝑛))[,)+∞) × ℝ)
= ((𝑒[,)+∞) ×
ℝ)) |
68 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) =
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) |
69 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒[,)+∞) ∈
V |
70 | 69, 21 | xpex 6860 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑒[,)+∞) × ℝ)
∈ V |
71 | 68, 70 | elrnmpti 5297 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ↔ ∃𝑒
∈ ℝ (((𝑥 /
(2↑𝑛))[,)+∞)
× ℝ) = ((𝑒[,)+∞) ×
ℝ)) |
72 | 67, 71 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ))) |
73 | 61, 72 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ (ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) |
74 | | elsigagen 29537 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V ∧ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ (ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) → (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
75 | 26, 73, 74 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
76 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
= ((((𝑥 + 1) /
(2↑𝑛))[,)+∞)
× ℝ) |
77 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑒 = ((𝑥 + 1) / (2↑𝑛)) → (𝑒[,)+∞) = (((𝑥 + 1) / (2↑𝑛))[,)+∞)) |
78 | 77 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑒 = ((𝑥 + 1) / (2↑𝑛)) → ((𝑒[,)+∞) × ℝ) = ((((𝑥 + 1) / (2↑𝑛))[,)+∞) ×
ℝ)) |
79 | 78 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 = ((𝑥 + 1) / (2↑𝑛)) → (((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) × ℝ)
↔ ((((𝑥 + 1) /
(2↑𝑛))[,)+∞)
× ℝ) = ((((𝑥 +
1) / (2↑𝑛))[,)+∞) ×
ℝ))) |
80 | 79 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑥 + 1) / (2↑𝑛)) ∈ ℝ ∧
((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
= ((((𝑥 + 1) /
(2↑𝑛))[,)+∞)
× ℝ)) → ∃𝑒 ∈ ℝ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) ×
ℝ)) |
81 | 48, 76, 80 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
∃𝑒 ∈ ℝ
((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
= ((𝑒[,)+∞) ×
ℝ)) |
82 | 68, 70 | elrnmpti 5297 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 + 1) /
(2↑𝑛))[,)+∞)
× ℝ) ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ↔
∃𝑒 ∈ ℝ
((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
= ((𝑒[,)+∞) ×
ℝ)) |
83 | 81, 82 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
∈ ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) ×
ℝ))) |
84 | 61, 83 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) |
85 | | elsigagen 29537 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V ∧ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) → ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
86 | 26, 84, 85 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
87 | | difelsiga 29523 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra ∧ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ∧ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) → ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∖
((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ))
∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
88 | 60, 75, 86, 87 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((((𝑥 / (2↑𝑛))[,)+∞) × ℝ)
∖ ((((𝑥 + 1) /
(2↑𝑛))[,)+∞)
× ℝ)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
89 | 59, 88 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
91 | 36, 90 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (𝑢 × ℝ) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) |
92 | 91 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → (𝑢 × ℝ) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))) |
93 | 92 | rexlimivv 3018 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℤ ∃𝑛 ∈
ℤ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → (𝑢 × ℝ) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) |
94 | 34, 93 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ran 𝐼 → (𝑢 × ℝ) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) |
95 | 32, 94 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ran 𝐼 → (◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
96 | 95 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
97 | | 2ndpreima 28868 |
. . . . . . . . . . . . 13
⊢ (𝑣 ⊆ ℝ → (◡(2nd ↾ (ℝ ×
ℝ)) “ 𝑣) =
(ℝ × 𝑣)) |
98 | 18, 97 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ran 𝐼 → (◡(2nd ↾ (ℝ ×
ℝ)) “ 𝑣) =
(ℝ × 𝑣)) |
99 | 2, 33 | elrnmpt2 6671 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ran 𝐼 ↔ ∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
100 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
101 | 100 | xpeq2d 5063 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (ℝ × 𝑣) = (ℝ × ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))) |
102 | | difxp2 5479 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℝ
× (((𝑥 /
(2↑𝑛))[,)+∞)
∖ (((𝑥 + 1) /
(2↑𝑛))[,)+∞))) =
((ℝ × ((𝑥 /
(2↑𝑛))[,)+∞))
∖ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞))) |
103 | 57 | xpeq2d 5063 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× (((𝑥 /
(2↑𝑛))[,)+∞)
∖ (((𝑥 + 1) /
(2↑𝑛))[,)+∞))) =
(ℝ × ((𝑥 /
(2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))) |
104 | 102, 103 | syl5reqr 2659 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) = ((ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∖ (ℝ ×
(((𝑥 + 1) / (2↑𝑛))[,)+∞)))) |
105 | | ssun2 3739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ⊆ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))) |
106 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)) |
107 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = (𝑥 / (2↑𝑛)) → (𝑓[,)+∞) = ((𝑥 / (2↑𝑛))[,)+∞)) |
108 | 107 | xpeq2d 5063 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = (𝑥 / (2↑𝑛)) → (ℝ × (𝑓[,)+∞)) = (ℝ ×
((𝑥 / (2↑𝑛))[,)+∞))) |
109 | 108 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = (𝑥 / (2↑𝑛)) → ((ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ × (𝑓[,)+∞)) ↔ (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)))) |
110 | 109 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 / (2↑𝑛)) ∈ ℝ ∧ (ℝ ×
((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞))) →
∃𝑓 ∈ ℝ
(ℝ × ((𝑥 /
(2↑𝑛))[,)+∞)) =
(ℝ × (𝑓[,)+∞))) |
111 | 44, 106, 110 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
∃𝑓 ∈ ℝ
(ℝ × ((𝑥 /
(2↑𝑛))[,)+∞)) =
(ℝ × (𝑓[,)+∞))) |
112 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ ℝ ↦ (ℝ
× (𝑓[,)+∞))) =
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) |
113 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓[,)+∞) ∈
V |
114 | 21, 113 | xpex 6860 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℝ
× (𝑓[,)+∞))
∈ V |
115 | 112, 114 | elrnmpti 5297 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)) ∈ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))) ↔ ∃𝑓 ∈ ℝ (ℝ ×
((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ
× (𝑓[,)+∞))) |
116 | 111, 115 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)) ∈ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))) |
117 | 105, 116 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)) ∈ (ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) |
118 | | elsigagen 29537 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V ∧ (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)) ∈ (ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) → (ℝ ×
((𝑥 / (2↑𝑛))[,)+∞)) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
119 | 26, 117, 118 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× ((𝑥 / (2↑𝑛))[,)+∞)) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
120 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℝ
× (((𝑥 + 1) /
(2↑𝑛))[,)+∞)) =
(ℝ × (((𝑥 + 1)
/ (2↑𝑛))[,)+∞)) |
121 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = ((𝑥 + 1) / (2↑𝑛)) → (𝑓[,)+∞) = (((𝑥 + 1) / (2↑𝑛))[,)+∞)) |
122 | 121 | xpeq2d 5063 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = ((𝑥 + 1) / (2↑𝑛)) → (ℝ × (𝑓[,)+∞)) = (ℝ ×
(((𝑥 + 1) / (2↑𝑛))[,)+∞))) |
123 | 122 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = ((𝑥 + 1) / (2↑𝑛)) → ((ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ
× (𝑓[,)+∞))
↔ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)))) |
124 | 123 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑥 + 1) / (2↑𝑛)) ∈ ℝ ∧ (ℝ
× (((𝑥 + 1) /
(2↑𝑛))[,)+∞)) =
(ℝ × (((𝑥 + 1)
/ (2↑𝑛))[,)+∞)))
→ ∃𝑓 ∈
ℝ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ × (𝑓[,)+∞))) |
125 | 48, 120, 124 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
∃𝑓 ∈ ℝ
(ℝ × (((𝑥 + 1)
/ (2↑𝑛))[,)+∞))
= (ℝ × (𝑓[,)+∞))) |
126 | 112, 114 | elrnmpti 5297 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℝ
× (((𝑥 + 1) /
(2↑𝑛))[,)+∞))
∈ ran (𝑓 ∈
ℝ ↦ (ℝ × (𝑓[,)+∞))) ↔ ∃𝑓 ∈ ℝ (ℝ ×
(((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ
× (𝑓[,)+∞))) |
127 | 125, 126 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× (((𝑥 + 1) /
(2↑𝑛))[,)+∞))
∈ ran (𝑓 ∈
ℝ ↦ (ℝ × (𝑓[,)+∞)))) |
128 | 105, 127 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× (((𝑥 + 1) /
(2↑𝑛))[,)+∞))
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) |
129 | | elsigagen 29537 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V ∧ (ℝ
× (((𝑥 + 1) /
(2↑𝑛))[,)+∞))
∈ (ran (𝑒 ∈
ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) → (ℝ ×
(((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
130 | 26, 128, 129 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× (((𝑥 + 1) /
(2↑𝑛))[,)+∞))
∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
131 | | difelsiga 29523 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra ∧ (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∧ (ℝ ×
(((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) → ((ℝ ×
((𝑥 / (2↑𝑛))[,)+∞)) ∖ (ℝ
× (((𝑥 + 1) /
(2↑𝑛))[,)+∞)))
∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
132 | 60, 119, 130, 131 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((ℝ × ((𝑥 /
(2↑𝑛))[,)+∞))
∖ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞))) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) |
133 | 104, 132 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ
× ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
134 | 133 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (ℝ × ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
135 | 101, 134 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (ℝ × 𝑣) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) |
136 | 135 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → (ℝ × 𝑣) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))) |
137 | 136 | rexlimivv 3018 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℤ ∃𝑛 ∈
ℤ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → (ℝ × 𝑣) ∈ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) |
138 | 99, 137 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ran 𝐼 → (ℝ × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
139 | 98, 138 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ran 𝐼 → (◡(2nd ↾ (ℝ ×
ℝ)) “ 𝑣) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
140 | 139 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (◡(2nd ↾ (ℝ ×
ℝ)) “ 𝑣) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
141 | | inelsiga 29525 |
. . . . . . . . . 10
⊢
(((sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra ∧ (◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞))))) ∧ (◡(2nd ↾ (ℝ ×
ℝ)) “ 𝑣) ∈
(sigaGen‘(ran (𝑒
∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) → ((◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) ∩
(◡(2nd ↾ (ℝ
× ℝ)) “ 𝑣)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
142 | 30, 96, 140, 141 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → ((◡(1st ↾ (ℝ ×
ℝ)) “ 𝑢) ∩
(◡(2nd ↾ (ℝ
× ℝ)) “ 𝑣)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
143 | 20, 142 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (𝑢 × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
144 | 143 | adantr 480 |
. . . . . . 7
⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → (𝑢 × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
145 | 11, 144 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → 𝑑 ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
146 | 145 | ex 449 |
. . . . 5
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (𝑑 = (𝑢 × 𝑣) → 𝑑 ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞))))))) |
147 | 146 | rexlimivv 3018 |
. . . 4
⊢
(∃𝑢 ∈ ran
𝐼∃𝑣 ∈ ran 𝐼 𝑑 = (𝑢 × 𝑣) → 𝑑 ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
148 | 10, 147 | sylbi 206 |
. . 3
⊢ (𝑑 ∈ ran 𝑅 → 𝑑 ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))))) |
149 | 148 | ssriv 3572 |
. 2
⊢ ran 𝑅 ⊆ (sigaGen‘(ran
(𝑒 ∈ ℝ ↦
((𝑒[,)+∞) ×
ℝ)) ∪ ran (𝑓
∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) |
150 | | sigagenss2 29540 |
. 2
⊢ ((∪ ran 𝑅 = ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))) ∧ ran 𝑅 ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞))))) ∧ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞)))) ∈ V) →
(sigaGen‘ran 𝑅)
⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran
(𝑓 ∈ ℝ ↦
(ℝ × (𝑓[,)+∞)))))) |
151 | 6, 149, 26, 150 | mp3an 1416 |
1
⊢
(sigaGen‘ran 𝑅) ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
∪ ran (𝑓 ∈ ℝ
↦ (ℝ × (𝑓[,)+∞))))) |