Metamath Proof Explorer

Theorem meaiuninclem

Description: Measures are continuous from below (bounded case): if E is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses meaiuninclem.m 
|- ( ph -> M e. Meas )
meaiuninclem.n 
|- ( ph -> N e. ZZ )
meaiuninclem.z 
|- Z = ( ZZ>= ` N )
meaiuninclem.e 
|- ( ph -> E : Z --> dom M )
meaiuninclem.i 
|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) )
meaiuninclem.b 
|- ( ph -> E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
meaiuninclem.s 
|- S = ( n e. Z |-> ( M ` ( E ` n ) ) )
meaiuninclem.f 
|- F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
Assertion meaiuninclem 
|- ( ph -> S ~~> ( M ` U_ n e. Z ( E ` n ) ) )

Proof

Step Hyp Ref Expression
1 meaiuninclem.m 
 |-  ( ph -> M e. Meas )
2 meaiuninclem.n 
 |-  ( ph -> N e. ZZ )
3 meaiuninclem.z 
 |-  Z = ( ZZ>= ` N )
4 meaiuninclem.e 
 |-  ( ph -> E : Z --> dom M )
5 meaiuninclem.i 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) )
6 meaiuninclem.b 
 |-  ( ph -> E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
7 meaiuninclem.s 
 |-  S = ( n e. Z |-> ( M ` ( E ` n ) ) )
8 meaiuninclem.f 
 |-  F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
9 0xr 
 |-  0 e. RR*
10 9 a1i 
 |-  ( ( ph /\ n e. Z ) -> 0 e. RR* )
11 pnfxr 
 |-  +oo e. RR*
12 11 a1i 
 |-  ( ( ph /\ n e. Z ) -> +oo e. RR* )
13 1 adantr 
 |-  ( ( ph /\ n e. Z ) -> M e. Meas )
14 eqid 
 |-  dom M = dom M
15 4 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) e. dom M )
16 13 14 15 meaxrcl 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) e. RR* )
17 13 15 meage0 
 |-  ( ( ph /\ n e. Z ) -> 0 <_ ( M ` ( E ` n ) ) )
18 6 adantr 
 |-  ( ( ph /\ n e. Z ) -> E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
19 simp1 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> ( ph /\ n e. Z ) )
20 simp2 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> x e. RR )
21 simp3 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> A. n e. Z ( M ` ( E ` n ) ) <_ x )
22 19 simprd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> n e. Z )
23 rspa 
 |-  ( ( A. n e. Z ( M ` ( E ` n ) ) <_ x /\ n e. Z ) -> ( M ` ( E ` n ) ) <_ x )
24 21 22 23 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> ( M ` ( E ` n ) ) <_ x )
25 16 3ad2ant1 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ ( M ` ( E ` n ) ) <_ x ) -> ( M ` ( E ` n ) ) e. RR* )
26 rexr 
 |-  ( x e. RR -> x e. RR* )
27 26 3ad2ant2 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ ( M ` ( E ` n ) ) <_ x ) -> x e. RR* )
28 11 a1i 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ ( M ` ( E ` n ) ) <_ x ) -> +oo e. RR* )
29 simp3 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ ( M ` ( E ` n ) ) <_ x ) -> ( M ` ( E ` n ) ) <_ x )
30 ltpnf 
 |-  ( x e. RR -> x < +oo )
31 30 3ad2ant2 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ ( M ` ( E ` n ) ) <_ x ) -> x < +oo )
32 25 27 28 29 31 xrlelttrd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ ( M ` ( E ` n ) ) <_ x ) -> ( M ` ( E ` n ) ) < +oo )
33 19 20 24 32 syl3anc 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. RR /\ A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> ( M ` ( E ` n ) ) < +oo )
34 33 3exp 
 |-  ( ( ph /\ n e. Z ) -> ( x e. RR -> ( A. n e. Z ( M ` ( E ` n ) ) <_ x -> ( M ` ( E ` n ) ) < +oo ) ) )
35 34 rexlimdv 
 |-  ( ( ph /\ n e. Z ) -> ( E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x -> ( M ` ( E ` n ) ) < +oo ) )
36 18 35 mpd 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) < +oo )
37 10 12 16 17 36 elicod 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) e. ( 0 [,) +oo ) )
38 37 7 fmptd 
 |-  ( ph -> S : Z --> ( 0 [,) +oo ) )
39 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
40 39 a1i 
 |-  ( ph -> ( 0 [,) +oo ) C_ RR )
41 38 40 fssd 
 |-  ( ph -> S : Z --> RR )
42 3 peano2uzs 
 |-  ( n e. Z -> ( n + 1 ) e. Z )
43 42 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( n + 1 ) e. Z )
44 4 ffvelcdmda 
 |-  ( ( ph /\ ( n + 1 ) e. Z ) -> ( E ` ( n + 1 ) ) e. dom M )
45 43 44 syldan 
 |-  ( ( ph /\ n e. Z ) -> ( E ` ( n + 1 ) ) e. dom M )
46 13 14 15 45 5 meassle 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) <_ ( M ` ( E ` ( n + 1 ) ) ) )
47 7 a1i 
 |-  ( ph -> S = ( n e. Z |-> ( M ` ( E ` n ) ) ) )
48 fvexd 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) e. _V )
49 47 48 fvmpt2d 
 |-  ( ( ph /\ n e. Z ) -> ( S ` n ) = ( M ` ( E ` n ) ) )
50 2fveq3 
 |-  ( n = m -> ( M ` ( E ` n ) ) = ( M ` ( E ` m ) ) )
51 50 cbvmptv 
 |-  ( n e. Z |-> ( M ` ( E ` n ) ) ) = ( m e. Z |-> ( M ` ( E ` m ) ) )
52 7 51 eqtri 
 |-  S = ( m e. Z |-> ( M ` ( E ` m ) ) )
53 2fveq3 
 |-  ( m = ( n + 1 ) -> ( M ` ( E ` m ) ) = ( M ` ( E ` ( n + 1 ) ) ) )
54 fvexd 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` ( n + 1 ) ) ) e. _V )
55 52 53 43 54 fvmptd3 
 |-  ( ( ph /\ n e. Z ) -> ( S ` ( n + 1 ) ) = ( M ` ( E ` ( n + 1 ) ) ) )
56 49 55 breq12d 
 |-  ( ( ph /\ n e. Z ) -> ( ( S ` n ) <_ ( S ` ( n + 1 ) ) <-> ( M ` ( E ` n ) ) <_ ( M ` ( E ` ( n + 1 ) ) ) ) )
57 46 56 mpbird 
 |-  ( ( ph /\ n e. Z ) -> ( S ` n ) <_ ( S ` ( n + 1 ) ) )
58 49 eqcomd 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) = ( S ` n ) )
59 58 breq1d 
 |-  ( ( ph /\ n e. Z ) -> ( ( M ` ( E ` n ) ) <_ x <-> ( S ` n ) <_ x ) )
60 59 ralbidva 
 |-  ( ph -> ( A. n e. Z ( M ` ( E ` n ) ) <_ x <-> A. n e. Z ( S ` n ) <_ x ) )
61 60 biimpd 
 |-  ( ph -> ( A. n e. Z ( M ` ( E ` n ) ) <_ x -> A. n e. Z ( S ` n ) <_ x ) )
62 61 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( A. n e. Z ( M ` ( E ` n ) ) <_ x -> A. n e. Z ( S ` n ) <_ x ) )
63 62 reximdva 
 |-  ( ph -> ( E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x -> E. x e. RR A. n e. Z ( S ` n ) <_ x ) )
64 6 63 mpd 
 |-  ( ph -> E. x e. RR A. n e. Z ( S ` n ) <_ x )
65 3 2 41 57 64 climsup 
 |-  ( ph -> S ~~> sup ( ran S , RR , < ) )
66 nfv 
 |-  F/ n ph
67 nfv 
 |-  F/ x ph
68 id 
 |-  ( n e. Z -> n e. Z )
69 fvex 
 |-  ( E ` n ) e. _V
70 69 difexi 
 |-  ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V
71 70 a1i 
 |-  ( n e. Z -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V )
72 8 fvmpt2 
 |-  ( ( n e. Z /\ ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V ) -> ( F ` n ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
73 68 71 72 syl2anc 
 |-  ( n e. Z -> ( F ` n ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
74 73 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
75 1 14 dmmeasal 
 |-  ( ph -> dom M e. SAlg )
76 75 adantr 
 |-  ( ( ph /\ n e. Z ) -> dom M e. SAlg )
77 fzoct 
 |-  ( N ..^ n ) ~<_ _om
78 77 a1i 
 |-  ( ( ph /\ n e. Z ) -> ( N ..^ n ) ~<_ _om )
79 4 adantr 
 |-  ( ( ph /\ i e. ( N ..^ n ) ) -> E : Z --> dom M )
80 fzossuz 
 |-  ( N ..^ n ) C_ ( ZZ>= ` N )
81 3 eqcomi 
 |-  ( ZZ>= ` N ) = Z
82 80 81 sseqtri 
 |-  ( N ..^ n ) C_ Z
83 82 sseli 
 |-  ( i e. ( N ..^ n ) -> i e. Z )
84 83 adantl 
 |-  ( ( ph /\ i e. ( N ..^ n ) ) -> i e. Z )
85 79 84 ffvelcdmd 
 |-  ( ( ph /\ i e. ( N ..^ n ) ) -> ( E ` i ) e. dom M )
86 85 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ i e. ( N ..^ n ) ) -> ( E ` i ) e. dom M )
87 76 78 86 saliuncl 
 |-  ( ( ph /\ n e. Z ) -> U_ i e. ( N ..^ n ) ( E ` i ) e. dom M )
88 saldifcl2 
 |-  ( ( dom M e. SAlg /\ ( E ` n ) e. dom M /\ U_ i e. ( N ..^ n ) ( E ` i ) e. dom M ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. dom M )
89 76 15 87 88 syl3anc 
 |-  ( ( ph /\ n e. Z ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. dom M )
90 74 89 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. dom M )
91 13 14 90 meaxrcl 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( F ` n ) ) e. RR* )
92 13 90 meage0 
 |-  ( ( ph /\ n e. Z ) -> 0 <_ ( M ` ( F ` n ) ) )
93 difssd 
 |-  ( ( ph /\ n e. Z ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) C_ ( E ` n ) )
94 74 93 eqsstrd 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) C_ ( E ` n ) )
95 13 14 90 15 94 meassle 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( F ` n ) ) <_ ( M ` ( E ` n ) ) )
96 91 16 12 95 36 xrlelttrd 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( F ` n ) ) < +oo )
97 10 12 91 92 96 elicod 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( F ` n ) ) e. ( 0 [,) +oo ) )
98 2fveq3 
 |-  ( n = i -> ( M ` ( E ` n ) ) = ( M ` ( E ` i ) ) )
99 98 breq1d 
 |-  ( n = i -> ( ( M ` ( E ` n ) ) <_ x <-> ( M ` ( E ` i ) ) <_ x ) )
100 99 cbvralvw 
 |-  ( A. n e. Z ( M ` ( E ` n ) ) <_ x <-> A. i e. Z ( M ` ( E ` i ) ) <_ x )
101 100 bilani 
 |-  ( ( ph /\ A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> A. i e. Z ( M ` ( E ` i ) ) <_ x )
102 eleq1w 
 |-  ( n = i -> ( n e. Z <-> i e. Z ) )
103 102 anbi2d 
 |-  ( n = i -> ( ( ph /\ n e. Z ) <-> ( ph /\ i e. Z ) ) )
104 oveq2 
 |-  ( n = i -> ( N ... n ) = ( N ... i ) )
105 104 sumeq1d 
 |-  ( n = i -> sum_ m e. ( N ... n ) ( M ` ( F ` m ) ) = sum_ m e. ( N ... i ) ( M ` ( F ` m ) ) )
106 98 105 eqeq12d 
 |-  ( n = i -> ( ( M ` ( E ` n ) ) = sum_ m e. ( N ... n ) ( M ` ( F ` m ) ) <-> ( M ` ( E ` i ) ) = sum_ m e. ( N ... i ) ( M ` ( F ` m ) ) ) )
107 103 106 imbi12d 
 |-  ( n = i -> ( ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) = sum_ m e. ( N ... n ) ( M ` ( F ` m ) ) ) <-> ( ( ph /\ i e. Z ) -> ( M ` ( E ` i ) ) = sum_ m e. ( N ... i ) ( M ` ( F ` m ) ) ) ) )
108 eleq1w 
 |-  ( m = n -> ( m e. Z <-> n e. Z ) )
109 108 anbi2d 
 |-  ( m = n -> ( ( ph /\ m e. Z ) <-> ( ph /\ n e. Z ) ) )
110 oveq2 
 |-  ( m = n -> ( N ... m ) = ( N ... n ) )
111 110 iuneq1d 
 |-  ( m = n -> U_ i e. ( N ... m ) ( F ` i ) = U_ i e. ( N ... n ) ( F ` i ) )
112 110 iuneq1d 
 |-  ( m = n -> U_ i e. ( N ... m ) ( E ` i ) = U_ i e. ( N ... n ) ( E ` i ) )
113 111 112 eqeq12d 
 |-  ( m = n -> ( U_ i e. ( N ... m ) ( F ` i ) = U_ i e. ( N ... m ) ( E ` i ) <-> U_ i e. ( N ... n ) ( F ` i ) = U_ i e. ( N ... n ) ( E ` i ) ) )
114 109 113 imbi12d 
 |-  ( m = n -> ( ( ( ph /\ m e. Z ) -> U_ i e. ( N ... m ) ( F ` i ) = U_ i e. ( N ... m ) ( E ` i ) ) <-> ( ( ph /\ n e. Z ) -> U_ i e. ( N ... n ) ( F ` i ) = U_ i e. ( N ... n ) ( E ` i ) ) ) )
115 fveq2 
 |-  ( i = n -> ( F ` i ) = ( F ` n ) )
116 115 cbviunv 
 |-  U_ i e. ( N ... m ) ( F ` i ) = U_ n e. ( N ... m ) ( F ` n )
117 116 a1i 
 |-  ( ( ph /\ m e. Z ) -> U_ i e. ( N ... m ) ( F ` i ) = U_ n e. ( N ... m ) ( F ` n ) )
118 66 3 4 8 iundjiun 
 |-  ( ph -> ( ( A. m e. Z U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) /\ U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) ) /\ Disj_ n e. Z ( F ` n ) ) )
119 118 simplld 
 |-  ( ph -> A. m e. Z U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) )
120 119 adantr 
 |-  ( ( ph /\ m e. Z ) -> A. m e. Z U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) )
121 simpr 
 |-  ( ( ph /\ m e. Z ) -> m e. Z )
122 rspa 
 |-  ( ( A. m e. Z U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) /\ m e. Z ) -> U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) )
123 120 121 122 syl2anc 
 |-  ( ( ph /\ m e. Z ) -> U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) )
124 fveq2 
 |-  ( n = i -> ( E ` n ) = ( E ` i ) )
125 124 cbviunv 
 |-  U_ n e. ( N ... m ) ( E ` n ) = U_ i e. ( N ... m ) ( E ` i )
126 125 a1i 
 |-  ( ( ph /\ m e. Z ) -> U_ n e. ( N ... m ) ( E ` n ) = U_ i e. ( N ... m ) ( E ` i ) )
127 117 123 126 3eqtrd 
 |-  ( ( ph /\ m e. Z ) -> U_ i e. ( N ... m ) ( F ` i ) = U_ i e. ( N ... m ) ( E ` i ) )
128 114 127 chvarvv 
 |-  ( ( ph /\ n e. Z ) -> U_ i e. ( N ... n ) ( F ` i ) = U_ i e. ( N ... n ) ( E ` i ) )
129 68 3 eleqtrdi 
 |-  ( n e. Z -> n e. ( ZZ>= ` N ) )
130 129 adantl 
 |-  ( ( ph /\ n e. Z ) -> n e. ( ZZ>= ` N ) )
131 fvoveq1 
 |-  ( n = i -> ( E ` ( n + 1 ) ) = ( E ` ( i + 1 ) ) )
132 124 131 sseq12d 
 |-  ( n = i -> ( ( E ` n ) C_ ( E ` ( n + 1 ) ) <-> ( E ` i ) C_ ( E ` ( i + 1 ) ) ) )
133 103 132 imbi12d 
 |-  ( n = i -> ( ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) ) <-> ( ( ph /\ i e. Z ) -> ( E ` i ) C_ ( E ` ( i + 1 ) ) ) ) )
134 133 5 chvarvv 
 |-  ( ( ph /\ i e. Z ) -> ( E ` i ) C_ ( E ` ( i + 1 ) ) )
135 84 134 syldan 
 |-  ( ( ph /\ i e. ( N ..^ n ) ) -> ( E ` i ) C_ ( E ` ( i + 1 ) ) )
136 135 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ i e. ( N ..^ n ) ) -> ( E ` i ) C_ ( E ` ( i + 1 ) ) )
137 130 136 iunincfi 
 |-  ( ( ph /\ n e. Z ) -> U_ i e. ( N ... n ) ( E ` i ) = ( E ` n ) )
138 128 137 eqtr2d 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) = U_ i e. ( N ... n ) ( F ` i ) )
139 138 fveq2d 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) = ( M ` U_ i e. ( N ... n ) ( F ` i ) ) )
140 nfv 
 |-  F/ i ( ph /\ n e. Z )
141 elfzuz 
 |-  ( i e. ( N ... n ) -> i e. ( ZZ>= ` N ) )
142 141 81 eleqtrdi 
 |-  ( i e. ( N ... n ) -> i e. Z )
143 142 adantl 
 |-  ( ( ph /\ i e. ( N ... n ) ) -> i e. Z )
144 fveq2 
 |-  ( n = i -> ( F ` n ) = ( F ` i ) )
145 144 eleq1d 
 |-  ( n = i -> ( ( F ` n ) e. dom M <-> ( F ` i ) e. dom M ) )
146 103 145 imbi12d 
 |-  ( n = i -> ( ( ( ph /\ n e. Z ) -> ( F ` n ) e. dom M ) <-> ( ( ph /\ i e. Z ) -> ( F ` i ) e. dom M ) ) )
147 146 90 chvarvv 
 |-  ( ( ph /\ i e. Z ) -> ( F ` i ) e. dom M )
148 143 147 syldan 
 |-  ( ( ph /\ i e. ( N ... n ) ) -> ( F ` i ) e. dom M )
149 148 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ i e. ( N ... n ) ) -> ( F ` i ) e. dom M )
150 fzct 
 |-  ( N ... n ) ~<_ _om
151 150 a1i 
 |-  ( ( ph /\ n e. Z ) -> ( N ... n ) ~<_ _om )
152 143 ssd 
 |-  ( ph -> ( N ... n ) C_ Z )
153 118 simprd 
 |-  ( ph -> Disj_ n e. Z ( F ` n ) )
154 144 cbvdisjv 
 |-  ( Disj_ n e. Z ( F ` n ) <-> Disj_ i e. Z ( F ` i ) )
155 153 154 sylib 
 |-  ( ph -> Disj_ i e. Z ( F ` i ) )
156 disjss1 
 |-  ( ( N ... n ) C_ Z -> ( Disj_ i e. Z ( F ` i ) -> Disj_ i e. ( N ... n ) ( F ` i ) ) )
157 152 155 156 sylc 
 |-  ( ph -> Disj_ i e. ( N ... n ) ( F ` i ) )
158 157 adantr 
 |-  ( ( ph /\ n e. Z ) -> Disj_ i e. ( N ... n ) ( F ` i ) )
159 140 13 14 149 151 158 meadjiun 
 |-  ( ( ph /\ n e. Z ) -> ( M ` U_ i e. ( N ... n ) ( F ` i ) ) = ( sum^ ` ( i e. ( N ... n ) |-> ( M ` ( F ` i ) ) ) ) )
160 fzfid 
 |-  ( ( ph /\ n e. Z ) -> ( N ... n ) e. Fin )
161 2fveq3 
 |-  ( n = i -> ( M ` ( F ` n ) ) = ( M ` ( F ` i ) ) )
162 161 eleq1d 
 |-  ( n = i -> ( ( M ` ( F ` n ) ) e. ( 0 [,) +oo ) <-> ( M ` ( F ` i ) ) e. ( 0 [,) +oo ) ) )
163 103 162 imbi12d 
 |-  ( n = i -> ( ( ( ph /\ n e. Z ) -> ( M ` ( F ` n ) ) e. ( 0 [,) +oo ) ) <-> ( ( ph /\ i e. Z ) -> ( M ` ( F ` i ) ) e. ( 0 [,) +oo ) ) ) )
164 163 97 chvarvv 
 |-  ( ( ph /\ i e. Z ) -> ( M ` ( F ` i ) ) e. ( 0 [,) +oo ) )
165 143 164 syldan 
 |-  ( ( ph /\ i e. ( N ... n ) ) -> ( M ` ( F ` i ) ) e. ( 0 [,) +oo ) )
166 165 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ i e. ( N ... n ) ) -> ( M ` ( F ` i ) ) e. ( 0 [,) +oo ) )
167 160 166 sge0fsummpt 
 |-  ( ( ph /\ n e. Z ) -> ( sum^ ` ( i e. ( N ... n ) |-> ( M ` ( F ` i ) ) ) ) = sum_ i e. ( N ... n ) ( M ` ( F ` i ) ) )
168 2fveq3 
 |-  ( i = m -> ( M ` ( F ` i ) ) = ( M ` ( F ` m ) ) )
169 168 cbvsumv 
 |-  sum_ i e. ( N ... n ) ( M ` ( F ` i ) ) = sum_ m e. ( N ... n ) ( M ` ( F ` m ) )
170 169 a1i 
 |-  ( ( ph /\ n e. Z ) -> sum_ i e. ( N ... n ) ( M ` ( F ` i ) ) = sum_ m e. ( N ... n ) ( M ` ( F ` m ) ) )
171 167 170 eqtrd 
 |-  ( ( ph /\ n e. Z ) -> ( sum^ ` ( i e. ( N ... n ) |-> ( M ` ( F ` i ) ) ) ) = sum_ m e. ( N ... n ) ( M ` ( F ` m ) ) )
172 139 159 171 3eqtrd 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) = sum_ m e. ( N ... n ) ( M ` ( F ` m ) ) )
173 107 172 chvarvv 
 |-  ( ( ph /\ i e. Z ) -> ( M ` ( E ` i ) ) = sum_ m e. ( N ... i ) ( M ` ( F ` m ) ) )
174 2fveq3 
 |-  ( m = n -> ( M ` ( F ` m ) ) = ( M ` ( F ` n ) ) )
175 174 cbvsumv 
 |-  sum_ m e. ( N ... i ) ( M ` ( F ` m ) ) = sum_ n e. ( N ... i ) ( M ` ( F ` n ) )
176 175 a1i 
 |-  ( ( ph /\ i e. Z ) -> sum_ m e. ( N ... i ) ( M ` ( F ` m ) ) = sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) )
177 173 176 eqtrd 
 |-  ( ( ph /\ i e. Z ) -> ( M ` ( E ` i ) ) = sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) )
178 177 breq1d 
 |-  ( ( ph /\ i e. Z ) -> ( ( M ` ( E ` i ) ) <_ x <-> sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) <_ x ) )
179 178 ralbidva 
 |-  ( ph -> ( A. i e. Z ( M ` ( E ` i ) ) <_ x <-> A. i e. Z sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) <_ x ) )
180 179 biimpd 
 |-  ( ph -> ( A. i e. Z ( M ` ( E ` i ) ) <_ x -> A. i e. Z sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) <_ x ) )
181 180 imp 
 |-  ( ( ph /\ A. i e. Z ( M ` ( E ` i ) ) <_ x ) -> A. i e. Z sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) <_ x )
182 101 181 syldan 
 |-  ( ( ph /\ A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> A. i e. Z sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) <_ x )
183 182 ex 
 |-  ( ph -> ( A. n e. Z ( M ` ( E ` n ) ) <_ x -> A. i e. Z sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) <_ x ) )
184 183 reximdv 
 |-  ( ph -> ( E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x -> E. x e. RR A. i e. Z sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) <_ x ) )
185 6 184 mpd 
 |-  ( ph -> E. x e. RR A. i e. Z sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) <_ x )
186 66 67 2 3 97 185 sge0reuzb 
 |-  ( ph -> ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) = sup ( ran ( i e. Z |-> sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) ) , RR , < ) )
187 98 cbvmptv 
 |-  ( n e. Z |-> ( M ` ( E ` n ) ) ) = ( i e. Z |-> ( M ` ( E ` i ) ) )
188 7 187 eqtri 
 |-  S = ( i e. Z |-> ( M ` ( E ` i ) ) )
189 188 a1i 
 |-  ( ph -> S = ( i e. Z |-> ( M ` ( E ` i ) ) ) )
190 177 mpteq2dva 
 |-  ( ph -> ( i e. Z |-> ( M ` ( E ` i ) ) ) = ( i e. Z |-> sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) ) )
191 189 190 eqtrd 
 |-  ( ph -> S = ( i e. Z |-> sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) ) )
192 191 rneqd 
 |-  ( ph -> ran S = ran ( i e. Z |-> sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) ) )
193 192 supeq1d 
 |-  ( ph -> sup ( ran S , RR , < ) = sup ( ran ( i e. Z |-> sum_ n e. ( N ... i ) ( M ` ( F ` n ) ) ) , RR , < ) )
194 186 193 eqtr4d 
 |-  ( ph -> ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) = sup ( ran S , RR , < ) )
195 194 eqcomd 
 |-  ( ph -> sup ( ran S , RR , < ) = ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) )
196 3 uzct 
 |-  Z ~<_ _om
197 196 a1i 
 |-  ( ph -> Z ~<_ _om )
198 66 1 14 90 197 153 meadjiun 
 |-  ( ph -> ( M ` U_ n e. Z ( F ` n ) ) = ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) )
199 198 eqcomd 
 |-  ( ph -> ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) = ( M ` U_ n e. Z ( F ` n ) ) )
200 118 simplrd 
 |-  ( ph -> U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) )
201 200 fveq2d 
 |-  ( ph -> ( M ` U_ n e. Z ( F ` n ) ) = ( M ` U_ n e. Z ( E ` n ) ) )
202 195 199 201 3eqtrd 
 |-  ( ph -> sup ( ran S , RR , < ) = ( M ` U_ n e. Z ( E ` n ) ) )
203 65 202 breqtrd 
 |-  ( ph -> S ~~> ( M ` U_ n e. Z ( E ` n ) ) )