Metamath Proof Explorer


Theorem sxbrsigalem2

Description: The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) is a subset of the sigma-algebra generated by the closed half-spaces of ( RR X. RR ) . The proof goes by noting the fact that the dyadic rectangles are intersections of a 'vertical band' and an 'horizontal band', which themselves are differences of closed half-spaces. (Contributed by Thierry Arnoux, 17-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0
|- J = ( topGen ` ran (,) )
dya2ioc.1
|- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
dya2ioc.2
|- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
Assertion sxbrsigalem2
|- ( sigaGen ` ran R ) C_ ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) )

Proof

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 ) ) ) ) )