Step |
Hyp |
Ref |
Expression |
1 |
|
sxbrsiga.0 |
⊢ 𝐽 = ( topGen ‘ ran (,) ) |
2 |
|
dya2ioc.1 |
⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
3 |
|
dya2ioc.2 |
⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) ) |
4 |
1 2 3
|
dya2iocucvr |
⊢ ∪ ran 𝑅 = ( ℝ × ℝ ) |
5 |
|
sxbrsigalem0 |
⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ℝ × ℝ ) |
6 |
4 5
|
eqtr4i |
⊢ ∪ ran 𝑅 = ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) |
7 |
|
vex |
⊢ 𝑢 ∈ V |
8 |
|
vex |
⊢ 𝑣 ∈ V |
9 |
7 8
|
xpex |
⊢ ( 𝑢 × 𝑣 ) ∈ V |
10 |
3 9
|
elrnmpo |
⊢ ( 𝑑 ∈ ran 𝑅 ↔ ∃ 𝑢 ∈ ran 𝐼 ∃ 𝑣 ∈ ran 𝐼 𝑑 = ( 𝑢 × 𝑣 ) ) |
11 |
|
simpr |
⊢ ( ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → 𝑑 = ( 𝑢 × 𝑣 ) ) |
12 |
1 2
|
dya2icobrsiga |
⊢ ran 𝐼 ⊆ 𝔅ℝ |
13 |
|
brsigasspwrn |
⊢ 𝔅ℝ ⊆ 𝒫 ℝ |
14 |
12 13
|
sstri |
⊢ ran 𝐼 ⊆ 𝒫 ℝ |
15 |
14
|
sseli |
⊢ ( 𝑢 ∈ ran 𝐼 → 𝑢 ∈ 𝒫 ℝ ) |
16 |
15
|
elpwid |
⊢ ( 𝑢 ∈ ran 𝐼 → 𝑢 ⊆ ℝ ) |
17 |
14
|
sseli |
⊢ ( 𝑣 ∈ ran 𝐼 → 𝑣 ∈ 𝒫 ℝ ) |
18 |
17
|
elpwid |
⊢ ( 𝑣 ∈ ran 𝐼 → 𝑣 ⊆ ℝ ) |
19 |
|
xpinpreima2 |
⊢ ( ( 𝑢 ⊆ ℝ ∧ 𝑣 ⊆ ℝ ) → ( 𝑢 × 𝑣 ) = ( ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∩ ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ) ) |
20 |
16 18 19
|
syl2an |
⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( 𝑢 × 𝑣 ) = ( ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∩ ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ) ) |
21 |
|
reex |
⊢ ℝ ∈ V |
22 |
21
|
mptex |
⊢ ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∈ V |
23 |
22
|
rnex |
⊢ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∈ V |
24 |
21
|
mptex |
⊢ ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ∈ V |
25 |
24
|
rnex |
⊢ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ∈ V |
26 |
23 25
|
unex |
⊢ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V |
27 |
26
|
a1i |
⊢ ( ⊤ → ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ) |
28 |
27
|
sgsiga |
⊢ ( ⊤ → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ∪ ran sigAlgebra ) |
29 |
28
|
mptru |
⊢ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ∪ ran sigAlgebra |
30 |
29
|
a1i |
⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ∪ ran sigAlgebra ) |
31 |
|
1stpreima |
⊢ ( 𝑢 ⊆ ℝ → ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) = ( 𝑢 × ℝ ) ) |
32 |
16 31
|
syl |
⊢ ( 𝑢 ∈ ran 𝐼 → ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) = ( 𝑢 × ℝ ) ) |
33 |
|
ovex |
⊢ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ V |
34 |
2 33
|
elrnmpo |
⊢ ( 𝑢 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
35 |
|
simpr |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
36 |
35
|
xpeq1d |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑢 × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) ) |
37 |
|
simpl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℤ ) |
38 |
37
|
zred |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ ) |
39 |
|
2rp |
⊢ 2 ∈ ℝ+ |
40 |
39
|
a1i |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 2 ∈ ℝ+ ) |
41 |
|
simpr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ ) |
42 |
40 41
|
rpexpcld |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 ↑ 𝑛 ) ∈ ℝ+ ) |
43 |
38 42
|
rerpdivcld |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ ) |
44 |
43
|
rexrd |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ) |
45 |
|
1red |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 1 ∈ ℝ ) |
46 |
38 45
|
readdcld |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 + 1 ) ∈ ℝ ) |
47 |
46 42
|
rerpdivcld |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ) |
48 |
47
|
rexrd |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ) |
49 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
50 |
49
|
a1i |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → +∞ ∈ ℝ* ) |
51 |
38
|
lep1d |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ≤ ( 𝑥 + 1 ) ) |
52 |
38 46 42 51
|
lediv1dd |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) |
53 |
|
pnfge |
⊢ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ ) |
54 |
48 53
|
syl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ ) |
55 |
|
difico |
⊢ ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ ) ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
56 |
44 48 50 52 54 55
|
syl32anc |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
57 |
56
|
xpeq1d |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) ) |
58 |
|
difxp1 |
⊢ ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) × ℝ ) = ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) |
59 |
57 58
|
eqtr3di |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) = ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) ) |
60 |
29
|
a1i |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ∪ ran sigAlgebra ) |
61 |
|
ssun1 |
⊢ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) |
62 |
|
eqid |
⊢ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) |
63 |
|
oveq1 |
⊢ ( 𝑒 = ( 𝑥 / ( 2 ↑ 𝑛 ) ) → ( 𝑒 [,) +∞ ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) |
64 |
63
|
xpeq1d |
⊢ ( 𝑒 = ( 𝑥 / ( 2 ↑ 𝑛 ) ) → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) |
65 |
64
|
rspceeqv |
⊢ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) → ∃ 𝑒 ∈ ℝ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) ) |
66 |
43 62 65
|
sylancl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑒 ∈ ℝ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) ) |
67 |
|
eqid |
⊢ ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) = ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) |
68 |
|
ovex |
⊢ ( 𝑒 [,) +∞ ) ∈ V |
69 |
68 21
|
xpex |
⊢ ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ V |
70 |
67 69
|
elrnmpti |
⊢ ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ↔ ∃ 𝑒 ∈ ℝ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) ) |
71 |
66 70
|
sylibr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ) |
72 |
61 71
|
sselid |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) |
73 |
|
elsigagen |
⊢ ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ∧ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
74 |
26 72 73
|
sylancr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
75 |
|
eqid |
⊢ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) |
76 |
|
oveq1 |
⊢ ( 𝑒 = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) → ( 𝑒 [,) +∞ ) = ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) |
77 |
76
|
xpeq1d |
⊢ ( 𝑒 = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) |
78 |
77
|
rspceeqv |
⊢ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) → ∃ 𝑒 ∈ ℝ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) ) |
79 |
47 75 78
|
sylancl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑒 ∈ ℝ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) ) |
80 |
67 69
|
elrnmpti |
⊢ ( ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ↔ ∃ 𝑒 ∈ ℝ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) ) |
81 |
79 80
|
sylibr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ) |
82 |
61 81
|
sselid |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) |
83 |
|
elsigagen |
⊢ ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ∧ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
84 |
26 82 83
|
sylancr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
85 |
|
difelsiga |
⊢ ( ( ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ∪ ran sigAlgebra ∧ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∧ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) → ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
86 |
60 74 84 85
|
syl3anc |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
87 |
59 86
|
eqeltrd |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
88 |
87
|
adantr |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
89 |
36 88
|
eqeltrd |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑢 × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
90 |
89
|
ex |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → ( 𝑢 × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) ) |
91 |
90
|
rexlimivv |
⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → ( 𝑢 × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
92 |
34 91
|
sylbi |
⊢ ( 𝑢 ∈ ran 𝐼 → ( 𝑢 × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
93 |
32 92
|
eqeltrd |
⊢ ( 𝑢 ∈ ran 𝐼 → ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
94 |
93
|
adantr |
⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
95 |
|
2ndpreima |
⊢ ( 𝑣 ⊆ ℝ → ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) = ( ℝ × 𝑣 ) ) |
96 |
18 95
|
syl |
⊢ ( 𝑣 ∈ ran 𝐼 → ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) = ( ℝ × 𝑣 ) ) |
97 |
2 33
|
elrnmpo |
⊢ ( 𝑣 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
98 |
|
simpr |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
99 |
98
|
xpeq2d |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ℝ × 𝑣 ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ) |
100 |
56
|
xpeq2d |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ) |
101 |
|
difxp2 |
⊢ ( ℝ × ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) = ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) |
102 |
100 101
|
eqtr3di |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) = ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) ) |
103 |
|
ssun2 |
⊢ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) |
104 |
|
eqid |
⊢ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) |
105 |
|
oveq1 |
⊢ ( 𝑓 = ( 𝑥 / ( 2 ↑ 𝑛 ) ) → ( 𝑓 [,) +∞ ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) |
106 |
105
|
xpeq2d |
⊢ ( 𝑓 = ( 𝑥 / ( 2 ↑ 𝑛 ) ) → ( ℝ × ( 𝑓 [,) +∞ ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) |
107 |
106
|
rspceeqv |
⊢ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) ) |
108 |
43 104 107
|
sylancl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) ) |
109 |
|
eqid |
⊢ ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) = ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) |
110 |
|
ovex |
⊢ ( 𝑓 [,) +∞ ) ∈ V |
111 |
21 110
|
xpex |
⊢ ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ V |
112 |
109 111
|
elrnmpti |
⊢ ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ↔ ∃ 𝑓 ∈ ℝ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) ) |
113 |
108 112
|
sylibr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) |
114 |
103 113
|
sselid |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) |
115 |
|
elsigagen |
⊢ ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ∧ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
116 |
26 114 115
|
sylancr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
117 |
|
eqid |
⊢ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) |
118 |
|
oveq1 |
⊢ ( 𝑓 = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) → ( 𝑓 [,) +∞ ) = ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) |
119 |
118
|
xpeq2d |
⊢ ( 𝑓 = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) → ( ℝ × ( 𝑓 [,) +∞ ) ) = ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) |
120 |
119
|
rspceeqv |
⊢ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) ) |
121 |
47 117 120
|
sylancl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) ) |
122 |
109 111
|
elrnmpti |
⊢ ( ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ↔ ∃ 𝑓 ∈ ℝ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) ) |
123 |
121 122
|
sylibr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) |
124 |
103 123
|
sselid |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) |
125 |
|
elsigagen |
⊢ ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ∧ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
126 |
26 124 125
|
sylancr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
127 |
|
difelsiga |
⊢ ( ( ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ∪ ran sigAlgebra ∧ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∧ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) → ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
128 |
60 116 126 127
|
syl3anc |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
129 |
102 128
|
eqeltrd |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
130 |
129
|
adantr |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
131 |
99 130
|
eqeltrd |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ℝ × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
132 |
131
|
ex |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → ( ℝ × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) ) |
133 |
132
|
rexlimivv |
⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → ( ℝ × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
134 |
97 133
|
sylbi |
⊢ ( 𝑣 ∈ ran 𝐼 → ( ℝ × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
135 |
96 134
|
eqeltrd |
⊢ ( 𝑣 ∈ ran 𝐼 → ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
136 |
135
|
adantl |
⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
137 |
|
inelsiga |
⊢ ( ( ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ∪ ran sigAlgebra ∧ ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∧ ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) → ( ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∩ ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
138 |
30 94 136 137
|
syl3anc |
⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( ( ◡ ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∩ ( ◡ ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
139 |
20 138
|
eqeltrd |
⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( 𝑢 × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
140 |
139
|
adantr |
⊢ ( ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → ( 𝑢 × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
141 |
11 140
|
eqeltrd |
⊢ ( ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → 𝑑 ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
142 |
141
|
ex |
⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( 𝑑 = ( 𝑢 × 𝑣 ) → 𝑑 ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) ) |
143 |
142
|
rexlimivv |
⊢ ( ∃ 𝑢 ∈ ran 𝐼 ∃ 𝑣 ∈ ran 𝐼 𝑑 = ( 𝑢 × 𝑣 ) → 𝑑 ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
144 |
10 143
|
sylbi |
⊢ ( 𝑑 ∈ ran 𝑅 → 𝑑 ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
145 |
144
|
ssriv |
⊢ ran 𝑅 ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) |
146 |
|
sigagenss2 |
⊢ ( ( ∪ ran 𝑅 = ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∧ ran 𝑅 ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∧ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ) → ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) |
147 |
6 145 26 146
|
mp3an |
⊢ ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) |