Step |
Hyp |
Ref |
Expression |
1 |
|
sxbrsiga.0 |
|- J = ( topGen ` ran (,) ) |
2 |
|
dya2ioc.1 |
|- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
3 |
|
dya2ioc.2 |
|- R = ( u e. ran I , v e. ran I |-> ( u X. v ) ) |
4 |
1 2 3
|
dya2iocucvr |
|- U. ran R = ( RR X. RR ) |
5 |
|
sxbrsigalem0 |
|- U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = ( RR X. RR ) |
6 |
4 5
|
eqtr4i |
|- U. ran R = U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) |
7 |
|
vex |
|- u e. _V |
8 |
|
vex |
|- v e. _V |
9 |
7 8
|
xpex |
|- ( u X. v ) e. _V |
10 |
3 9
|
elrnmpo |
|- ( d e. ran R <-> E. u e. ran I E. v e. ran I d = ( u X. v ) ) |
11 |
|
simpr |
|- ( ( ( u e. ran I /\ v e. ran I ) /\ d = ( u X. v ) ) -> d = ( u X. v ) ) |
12 |
1 2
|
dya2icobrsiga |
|- ran I C_ BrSiga |
13 |
|
brsigasspwrn |
|- BrSiga C_ ~P RR |
14 |
12 13
|
sstri |
|- ran I C_ ~P RR |
15 |
14
|
sseli |
|- ( u e. ran I -> u e. ~P RR ) |
16 |
15
|
elpwid |
|- ( u e. ran I -> u C_ RR ) |
17 |
14
|
sseli |
|- ( v e. ran I -> v e. ~P RR ) |
18 |
17
|
elpwid |
|- ( v e. ran I -> v C_ RR ) |
19 |
|
xpinpreima2 |
|- ( ( u C_ RR /\ v C_ RR ) -> ( u X. v ) = ( ( `' ( 1st |` ( RR X. RR ) ) " u ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " v ) ) ) |
20 |
16 18 19
|
syl2an |
|- ( ( u e. ran I /\ v e. ran I ) -> ( u X. v ) = ( ( `' ( 1st |` ( RR X. RR ) ) " u ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " v ) ) ) |
21 |
|
reex |
|- RR e. _V |
22 |
21
|
mptex |
|- ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) e. _V |
23 |
22
|
rnex |
|- ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) e. _V |
24 |
21
|
mptex |
|- ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) e. _V |
25 |
24
|
rnex |
|- ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) e. _V |
26 |
23 25
|
unex |
|- ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) e. _V |
27 |
26
|
a1i |
|- ( T. -> ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) e. _V ) |
28 |
27
|
sgsiga |
|- ( T. -> ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) e. U. ran sigAlgebra ) |
29 |
28
|
mptru |
|- ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) e. U. ran sigAlgebra |
30 |
29
|
a1i |
|- ( ( u e. ran I /\ v e. ran I ) -> ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) e. U. ran sigAlgebra ) |
31 |
|
1stpreima |
|- ( u C_ RR -> ( `' ( 1st |` ( RR X. RR ) ) " u ) = ( u X. RR ) ) |
32 |
16 31
|
syl |
|- ( u e. ran I -> ( `' ( 1st |` ( RR X. RR ) ) " u ) = ( u X. RR ) ) |
33 |
|
ovex |
|- ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. _V |
34 |
2 33
|
elrnmpo |
|- ( u e. ran I <-> E. x e. ZZ E. n e. ZZ u = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
35 |
|
simpr |
|- ( ( ( x e. ZZ /\ n e. ZZ ) /\ u = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> u = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
36 |
35
|
xpeq1d |
|- ( ( ( x e. ZZ /\ n e. ZZ ) /\ u = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( u X. RR ) = ( ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) X. RR ) ) |
37 |
|
simpl |
|- ( ( x e. ZZ /\ n e. ZZ ) -> x e. ZZ ) |
38 |
37
|
zred |
|- ( ( x e. ZZ /\ n e. ZZ ) -> x e. RR ) |
39 |
|
2rp |
|- 2 e. RR+ |
40 |
39
|
a1i |
|- ( ( x e. ZZ /\ n e. ZZ ) -> 2 e. RR+ ) |
41 |
|
simpr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> n e. ZZ ) |
42 |
40 41
|
rpexpcld |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( 2 ^ n ) e. RR+ ) |
43 |
38 42
|
rerpdivcld |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( x / ( 2 ^ n ) ) e. RR ) |
44 |
43
|
rexrd |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( x / ( 2 ^ n ) ) e. RR* ) |
45 |
|
1red |
|- ( ( x e. ZZ /\ n e. ZZ ) -> 1 e. RR ) |
46 |
38 45
|
readdcld |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( x + 1 ) e. RR ) |
47 |
46 42
|
rerpdivcld |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( x + 1 ) / ( 2 ^ n ) ) e. RR ) |
48 |
47
|
rexrd |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( x + 1 ) / ( 2 ^ n ) ) e. RR* ) |
49 |
|
pnfxr |
|- +oo e. RR* |
50 |
49
|
a1i |
|- ( ( x e. ZZ /\ n e. ZZ ) -> +oo e. RR* ) |
51 |
38
|
lep1d |
|- ( ( x e. ZZ /\ n e. ZZ ) -> x <_ ( x + 1 ) ) |
52 |
38 46 42 51
|
lediv1dd |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( x / ( 2 ^ n ) ) <_ ( ( x + 1 ) / ( 2 ^ n ) ) ) |
53 |
|
pnfge |
|- ( ( ( x + 1 ) / ( 2 ^ n ) ) e. RR* -> ( ( x + 1 ) / ( 2 ^ n ) ) <_ +oo ) |
54 |
48 53
|
syl |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( x + 1 ) / ( 2 ^ n ) ) <_ +oo ) |
55 |
|
difico |
|- ( ( ( ( x / ( 2 ^ n ) ) e. RR* /\ ( ( x + 1 ) / ( 2 ^ n ) ) e. RR* /\ +oo e. RR* ) /\ ( ( x / ( 2 ^ n ) ) <_ ( ( x + 1 ) / ( 2 ^ n ) ) /\ ( ( x + 1 ) / ( 2 ^ n ) ) <_ +oo ) ) -> ( ( ( x / ( 2 ^ n ) ) [,) +oo ) \ ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
56 |
44 48 50 52 54 55
|
syl32anc |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( x / ( 2 ^ n ) ) [,) +oo ) \ ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
57 |
56
|
xpeq1d |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( ( x / ( 2 ^ n ) ) [,) +oo ) \ ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) X. RR ) = ( ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) X. RR ) ) |
58 |
|
difxp1 |
|- ( ( ( ( x / ( 2 ^ n ) ) [,) +oo ) \ ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) X. RR ) = ( ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) \ ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) ) |
59 |
57 58
|
eqtr3di |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) X. RR ) = ( ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) \ ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) ) ) |
60 |
29
|
a1i |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) e. U. ran sigAlgebra ) |
61 |
|
ssun1 |
|- ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) C_ ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) |
62 |
|
eqid |
|- ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) |
63 |
|
oveq1 |
|- ( e = ( x / ( 2 ^ n ) ) -> ( e [,) +oo ) = ( ( x / ( 2 ^ n ) ) [,) +oo ) ) |
64 |
63
|
xpeq1d |
|- ( e = ( x / ( 2 ^ n ) ) -> ( ( e [,) +oo ) X. RR ) = ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) ) |
65 |
64
|
rspceeqv |
|- ( ( ( x / ( 2 ^ n ) ) e. RR /\ ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) ) -> E. e e. RR ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( e [,) +oo ) X. RR ) ) |
66 |
43 62 65
|
sylancl |
|- ( ( x e. ZZ /\ n e. ZZ ) -> E. e e. RR ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( e [,) +oo ) X. RR ) ) |
67 |
|
eqid |
|- ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) = ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) |
68 |
|
ovex |
|- ( e [,) +oo ) e. _V |
69 |
68 21
|
xpex |
|- ( ( e [,) +oo ) X. RR ) e. _V |
70 |
67 69
|
elrnmpti |
|- ( ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) <-> E. e e. RR ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( e [,) +oo ) X. RR ) ) |
71 |
66 70
|
sylibr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ) |
72 |
61 71
|
sselid |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) |
73 |
|
elsigagen |
|- ( ( ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) e. _V /\ ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) -> ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
74 |
26 72 73
|
sylancr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
75 |
|
eqid |
|- ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) |
76 |
|
oveq1 |
|- ( e = ( ( x + 1 ) / ( 2 ^ n ) ) -> ( e [,) +oo ) = ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) |
77 |
76
|
xpeq1d |
|- ( e = ( ( x + 1 ) / ( 2 ^ n ) ) -> ( ( e [,) +oo ) X. RR ) = ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) ) |
78 |
77
|
rspceeqv |
|- ( ( ( ( x + 1 ) / ( 2 ^ n ) ) e. RR /\ ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) ) -> E. e e. RR ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( e [,) +oo ) X. RR ) ) |
79 |
47 75 78
|
sylancl |
|- ( ( x e. ZZ /\ n e. ZZ ) -> E. e e. RR ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( e [,) +oo ) X. RR ) ) |
80 |
67 69
|
elrnmpti |
|- ( ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) <-> E. e e. RR ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) = ( ( e [,) +oo ) X. RR ) ) |
81 |
79 80
|
sylibr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ) |
82 |
61 81
|
sselid |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) |
83 |
|
elsigagen |
|- ( ( ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) e. _V /\ ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) -> ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
84 |
26 82 83
|
sylancr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
85 |
|
difelsiga |
|- ( ( ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) e. U. ran sigAlgebra /\ ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) /\ ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) -> ( ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) \ ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
86 |
60 74 84 85
|
syl3anc |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( ( x / ( 2 ^ n ) ) [,) +oo ) X. RR ) \ ( ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) X. RR ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
87 |
59 86
|
eqeltrd |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
88 |
87
|
adantr |
|- ( ( ( x e. ZZ /\ n e. ZZ ) /\ u = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
89 |
36 88
|
eqeltrd |
|- ( ( ( x e. ZZ /\ n e. ZZ ) /\ u = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( u X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
90 |
89
|
ex |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( u = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) -> ( u X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) ) |
91 |
90
|
rexlimivv |
|- ( E. x e. ZZ E. n e. ZZ u = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) -> ( u X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
92 |
34 91
|
sylbi |
|- ( u e. ran I -> ( u X. RR ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
93 |
32 92
|
eqeltrd |
|- ( u e. ran I -> ( `' ( 1st |` ( RR X. RR ) ) " u ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
94 |
93
|
adantr |
|- ( ( u e. ran I /\ v e. ran I ) -> ( `' ( 1st |` ( RR X. RR ) ) " u ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
95 |
|
2ndpreima |
|- ( v C_ RR -> ( `' ( 2nd |` ( RR X. RR ) ) " v ) = ( RR X. v ) ) |
96 |
18 95
|
syl |
|- ( v e. ran I -> ( `' ( 2nd |` ( RR X. RR ) ) " v ) = ( RR X. v ) ) |
97 |
2 33
|
elrnmpo |
|- ( v e. ran I <-> E. x e. ZZ E. n e. ZZ v = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
98 |
|
simpr |
|- ( ( ( x e. ZZ /\ n e. ZZ ) /\ v = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> v = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
99 |
98
|
xpeq2d |
|- ( ( ( x e. ZZ /\ n e. ZZ ) /\ v = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( RR X. v ) = ( RR X. ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) ) |
100 |
56
|
xpeq2d |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( ( x / ( 2 ^ n ) ) [,) +oo ) \ ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) ) = ( RR X. ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) ) |
101 |
|
difxp2 |
|- ( RR X. ( ( ( x / ( 2 ^ n ) ) [,) +oo ) \ ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) ) = ( ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) \ ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) ) |
102 |
100 101
|
eqtr3di |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) = ( ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) \ ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) ) ) |
103 |
|
ssun2 |
|- ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) C_ ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) |
104 |
|
eqid |
|- ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) |
105 |
|
oveq1 |
|- ( f = ( x / ( 2 ^ n ) ) -> ( f [,) +oo ) = ( ( x / ( 2 ^ n ) ) [,) +oo ) ) |
106 |
105
|
xpeq2d |
|- ( f = ( x / ( 2 ^ n ) ) -> ( RR X. ( f [,) +oo ) ) = ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) ) |
107 |
106
|
rspceeqv |
|- ( ( ( x / ( 2 ^ n ) ) e. RR /\ ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) ) -> E. f e. RR ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( f [,) +oo ) ) ) |
108 |
43 104 107
|
sylancl |
|- ( ( x e. ZZ /\ n e. ZZ ) -> E. f e. RR ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( f [,) +oo ) ) ) |
109 |
|
eqid |
|- ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) = ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) |
110 |
|
ovex |
|- ( f [,) +oo ) e. _V |
111 |
21 110
|
xpex |
|- ( RR X. ( f [,) +oo ) ) e. _V |
112 |
109 111
|
elrnmpti |
|- ( ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) e. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) <-> E. f e. RR ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( f [,) +oo ) ) ) |
113 |
108 112
|
sylibr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) e. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) |
114 |
103 113
|
sselid |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) |
115 |
|
elsigagen |
|- ( ( ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) e. _V /\ ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) -> ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
116 |
26 114 115
|
sylancr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
117 |
|
eqid |
|- ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) |
118 |
|
oveq1 |
|- ( f = ( ( x + 1 ) / ( 2 ^ n ) ) -> ( f [,) +oo ) = ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) |
119 |
118
|
xpeq2d |
|- ( f = ( ( x + 1 ) / ( 2 ^ n ) ) -> ( RR X. ( f [,) +oo ) ) = ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) ) |
120 |
119
|
rspceeqv |
|- ( ( ( ( x + 1 ) / ( 2 ^ n ) ) e. RR /\ ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) ) -> E. f e. RR ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( f [,) +oo ) ) ) |
121 |
47 117 120
|
sylancl |
|- ( ( x e. ZZ /\ n e. ZZ ) -> E. f e. RR ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( f [,) +oo ) ) ) |
122 |
109 111
|
elrnmpti |
|- ( ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) e. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) <-> E. f e. RR ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) = ( RR X. ( f [,) +oo ) ) ) |
123 |
121 122
|
sylibr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) e. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) |
124 |
103 123
|
sselid |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) |
125 |
|
elsigagen |
|- ( ( ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) e. _V /\ ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) -> ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
126 |
26 124 125
|
sylancr |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
127 |
|
difelsiga |
|- ( ( ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) e. U. ran sigAlgebra /\ ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) /\ ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) -> ( ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) \ ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
128 |
60 116 126 127
|
syl3anc |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( ( RR X. ( ( x / ( 2 ^ n ) ) [,) +oo ) ) \ ( RR X. ( ( ( x + 1 ) / ( 2 ^ n ) ) [,) +oo ) ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
129 |
102 128
|
eqeltrd |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( RR X. ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
130 |
129
|
adantr |
|- ( ( ( x e. ZZ /\ n e. ZZ ) /\ v = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( RR X. ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
131 |
99 130
|
eqeltrd |
|- ( ( ( x e. ZZ /\ n e. ZZ ) /\ v = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( RR X. v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
132 |
131
|
ex |
|- ( ( x e. ZZ /\ n e. ZZ ) -> ( v = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) -> ( RR X. v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) ) |
133 |
132
|
rexlimivv |
|- ( E. x e. ZZ E. n e. ZZ v = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) -> ( RR X. v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
134 |
97 133
|
sylbi |
|- ( v e. ran I -> ( RR X. v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
135 |
96 134
|
eqeltrd |
|- ( v e. ran I -> ( `' ( 2nd |` ( RR X. RR ) ) " v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
136 |
135
|
adantl |
|- ( ( u e. ran I /\ v e. ran I ) -> ( `' ( 2nd |` ( RR X. RR ) ) " v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
137 |
|
inelsiga |
|- ( ( ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) e. U. ran sigAlgebra /\ ( `' ( 1st |` ( RR X. RR ) ) " u ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) /\ ( `' ( 2nd |` ( RR X. RR ) ) " v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) -> ( ( `' ( 1st |` ( RR X. RR ) ) " u ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " v ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
138 |
30 94 136 137
|
syl3anc |
|- ( ( u e. ran I /\ v e. ran I ) -> ( ( `' ( 1st |` ( RR X. RR ) ) " u ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " v ) ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
139 |
20 138
|
eqeltrd |
|- ( ( u e. ran I /\ v e. ran I ) -> ( u X. v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
140 |
139
|
adantr |
|- ( ( ( u e. ran I /\ v e. ran I ) /\ d = ( u X. v ) ) -> ( u X. v ) e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
141 |
11 140
|
eqeltrd |
|- ( ( ( u e. ran I /\ v e. ran I ) /\ d = ( u X. v ) ) -> d e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
142 |
141
|
ex |
|- ( ( u e. ran I /\ v e. ran I ) -> ( d = ( u X. v ) -> d e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) ) |
143 |
142
|
rexlimivv |
|- ( E. u e. ran I E. v e. ran I d = ( u X. v ) -> d e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
144 |
10 143
|
sylbi |
|- ( d e. ran R -> d e. ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
145 |
144
|
ssriv |
|- ran R C_ ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) |
146 |
|
sigagenss2 |
|- ( ( U. ran R = U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) /\ ran R C_ ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) /\ ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) e. _V ) -> ( sigaGen ` ran R ) C_ ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) ) |
147 |
6 145 26 146
|
mp3an |
|- ( sigaGen ` ran R ) C_ ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) |