Step |
Hyp |
Ref |
Expression |
1 |
|
meaiuninc.m |
|- ( ph -> M e. Meas ) |
2 |
|
meaiuninc.n |
|- ( ph -> N e. ZZ ) |
3 |
|
meaiuninc.z |
|- Z = ( ZZ>= ` N ) |
4 |
|
meaiuninc.e |
|- ( ph -> E : Z --> dom M ) |
5 |
|
meaiuninc.i |
|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) ) |
6 |
|
meaiuninc.x |
|- ( ph -> E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) |
7 |
|
meaiuninc.s |
|- S = ( n e. Z |-> ( M ` ( E ` n ) ) ) |
8 |
|
2fveq3 |
|- ( n = m -> ( M ` ( E ` n ) ) = ( M ` ( E ` m ) ) ) |
9 |
8
|
cbvmptv |
|- ( n e. Z |-> ( M ` ( E ` n ) ) ) = ( m e. Z |-> ( M ` ( E ` m ) ) ) |
10 |
7 9
|
eqtri |
|- S = ( m e. Z |-> ( M ` ( E ` m ) ) ) |
11 |
10
|
a1i |
|- ( ph -> S = ( m e. Z |-> ( M ` ( E ` m ) ) ) ) |
12 |
10 7
|
eqtr3i |
|- ( m e. Z |-> ( M ` ( E ` m ) ) ) = ( n e. Z |-> ( M ` ( E ` n ) ) ) |
13 |
|
fveq2 |
|- ( k = i -> ( E ` k ) = ( E ` i ) ) |
14 |
13
|
cbviunv |
|- U_ k e. ( N ..^ m ) ( E ` k ) = U_ i e. ( N ..^ m ) ( E ` i ) |
15 |
14
|
difeq2i |
|- ( ( E ` m ) \ U_ k e. ( N ..^ m ) ( E ` k ) ) = ( ( E ` m ) \ U_ i e. ( N ..^ m ) ( E ` i ) ) |
16 |
15
|
mpteq2i |
|- ( m e. Z |-> ( ( E ` m ) \ U_ k e. ( N ..^ m ) ( E ` k ) ) ) = ( m e. Z |-> ( ( E ` m ) \ U_ i e. ( N ..^ m ) ( E ` i ) ) ) |
17 |
|
fveq2 |
|- ( m = n -> ( E ` m ) = ( E ` n ) ) |
18 |
|
oveq2 |
|- ( m = n -> ( N ..^ m ) = ( N ..^ n ) ) |
19 |
18
|
iuneq1d |
|- ( m = n -> U_ i e. ( N ..^ m ) ( E ` i ) = U_ i e. ( N ..^ n ) ( E ` i ) ) |
20 |
17 19
|
difeq12d |
|- ( m = n -> ( ( E ` m ) \ U_ i e. ( N ..^ m ) ( E ` i ) ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) ) |
21 |
20
|
cbvmptv |
|- ( m e. Z |-> ( ( E ` m ) \ U_ i e. ( N ..^ m ) ( E ` i ) ) ) = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) ) |
22 |
16 21
|
eqtri |
|- ( m e. Z |-> ( ( E ` m ) \ U_ k e. ( N ..^ m ) ( E ` k ) ) ) = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) ) |
23 |
1 2 3 4 5 6 12 22
|
meaiuninclem |
|- ( ph -> ( m e. Z |-> ( M ` ( E ` m ) ) ) ~~> ( M ` U_ n e. Z ( E ` n ) ) ) |
24 |
11 23
|
eqbrtrd |
|- ( ph -> S ~~> ( M ` U_ n e. Z ( E ` n ) ) ) |