Metamath Proof Explorer

Theorem carageniuncllem2

Description: The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses carageniuncllem2.o 
|- ( ph -> O e. OutMeas )
carageniuncllem2.s 
|- S = ( CaraGen ` O )
carageniuncllem2.x 
|- X = U. dom O
carageniuncllem2.a 
|- ( ph -> A C_ X )
carageniuncllem2.re 
|- ( ph -> ( O ` A ) e. RR )
carageniuncllem2.m 
|- ( ph -> M e. ZZ )
carageniuncllem2.z 
|- Z = ( ZZ>= ` M )
carageniuncllem2.e 
|- ( ph -> E : Z --> S )
carageniuncllem2.y 
|- ( ph -> Y e. RR+ )
carageniuncllem2.g 
|- G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )
carageniuncllem2.f 
|- F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) )
Assertion carageniuncllem2 
|- ( ph -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` A ) + Y ) )

Proof

Step Hyp Ref Expression
1 carageniuncllem2.o 
 |-  ( ph -> O e. OutMeas )
2 carageniuncllem2.s 
 |-  S = ( CaraGen ` O )
3 carageniuncllem2.x 
 |-  X = U. dom O
4 carageniuncllem2.a 
 |-  ( ph -> A C_ X )
5 carageniuncllem2.re 
 |-  ( ph -> ( O ` A ) e. RR )
6 carageniuncllem2.m 
 |-  ( ph -> M e. ZZ )
7 carageniuncllem2.z 
 |-  Z = ( ZZ>= ` M )
8 carageniuncllem2.e 
 |-  ( ph -> E : Z --> S )
9 carageniuncllem2.y 
 |-  ( ph -> Y e. RR+ )
10 carageniuncllem2.g 
 |-  G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )
11 carageniuncllem2.f 
 |-  F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) )
12 inss1 
 |-  ( A i^i U_ n e. Z ( E ` n ) ) C_ A
13 12 a1i 
 |-  ( ph -> ( A i^i U_ n e. Z ( E ` n ) ) C_ A )
14 1 3 4 5 13 omessre 
 |-  ( ph -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) e. RR )
15 difssd 
 |-  ( ph -> ( A \ U_ n e. Z ( E ` n ) ) C_ A )
16 1 3 4 5 15 omessre 
 |-  ( ph -> ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) e. RR )
17 rexadd 
 |-  ( ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) e. RR /\ ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) e. RR ) -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) = ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) + ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) )
18 14 16 17 syl2anc 
 |-  ( ph -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) = ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) + ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) )
19 ssinss1 
 |-  ( A C_ X -> ( A i^i ( F ` n ) ) C_ X )
20 4 19 syl 
 |-  ( ph -> ( A i^i ( F ` n ) ) C_ X )
21 1 3 unidmex 
 |-  ( ph -> X e. _V )
22 ssexg 
 |-  ( ( A C_ X /\ X e. _V ) -> A e. _V )
23 4 21 22 syl2anc 
 |-  ( ph -> A e. _V )
24 inex1g 
 |-  ( A e. _V -> ( A i^i ( F ` n ) ) e. _V )
25 23 24 syl 
 |-  ( ph -> ( A i^i ( F ` n ) ) e. _V )
26 elpwg 
 |-  ( ( A i^i ( F ` n ) ) e. _V -> ( ( A i^i ( F ` n ) ) e. ~P X <-> ( A i^i ( F ` n ) ) C_ X ) )
27 25 26 syl 
 |-  ( ph -> ( ( A i^i ( F ` n ) ) e. ~P X <-> ( A i^i ( F ` n ) ) C_ X ) )
28 20 27 mpbird 
 |-  ( ph -> ( A i^i ( F ` n ) ) e. ~P X )
29 28 adantr 
 |-  ( ( ph /\ n e. Z ) -> ( A i^i ( F ` n ) ) e. ~P X )
30 eqid 
 |-  ( n e. Z |-> ( A i^i ( F ` n ) ) ) = ( n e. Z |-> ( A i^i ( F ` n ) ) )
31 29 30 fmptd 
 |-  ( ph -> ( n e. Z |-> ( A i^i ( F ` n ) ) ) : Z --> ~P X )
32 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
33 32 ineq2d 
 |-  ( k = n -> ( A i^i ( F ` k ) ) = ( A i^i ( F ` n ) ) )
34 33 cbvmptv 
 |-  ( k e. Z |-> ( A i^i ( F ` k ) ) ) = ( n e. Z |-> ( A i^i ( F ` n ) ) )
35 34 feq1i 
 |-  ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) : Z --> ~P X <-> ( n e. Z |-> ( A i^i ( F ` n ) ) ) : Z --> ~P X )
36 35 a1i 
 |-  ( ph -> ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) : Z --> ~P X <-> ( n e. Z |-> ( A i^i ( F ` n ) ) ) : Z --> ~P X ) )
37 31 36 mpbird 
 |-  ( ph -> ( k e. Z |-> ( A i^i ( F ` k ) ) ) : Z --> ~P X )
38 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
39 25 adantr 
 |-  ( ( ph /\ n e. Z ) -> ( A i^i ( F ` n ) ) e. _V )
40 34 fvmpt2 
 |-  ( ( n e. Z /\ ( A i^i ( F ` n ) ) e. _V ) -> ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) = ( A i^i ( F ` n ) ) )
41 38 39 40 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) = ( A i^i ( F ` n ) ) )
42 41 iuneq2dv 
 |-  ( ph -> U_ n e. Z ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) = U_ n e. Z ( A i^i ( F ` n ) ) )
43 42 fveq2d 
 |-  ( ph -> ( O ` U_ n e. Z ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) = ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) )
44 nfv 
 |-  F/ n ph
45 44 7 8 11 iundjiun 
 |-  ( ph -> ( ( A. m e. Z U_ n e. ( M ... m ) ( F ` n ) = U_ n e. ( M ... m ) ( E ` n ) /\ U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) ) /\ Disj_ n e. Z ( F ` n ) ) )
46 45 simplrd 
 |-  ( ph -> U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) )
47 46 eqcomd 
 |-  ( ph -> U_ n e. Z ( E ` n ) = U_ n e. Z ( F ` n ) )
48 47 ineq2d 
 |-  ( ph -> ( A i^i U_ n e. Z ( E ` n ) ) = ( A i^i U_ n e. Z ( F ` n ) ) )
49 iunin2 
 |-  U_ n e. Z ( A i^i ( F ` n ) ) = ( A i^i U_ n e. Z ( F ` n ) )
50 49 eqcomi 
 |-  ( A i^i U_ n e. Z ( F ` n ) ) = U_ n e. Z ( A i^i ( F ` n ) )
51 50 a1i 
 |-  ( ph -> ( A i^i U_ n e. Z ( F ` n ) ) = U_ n e. Z ( A i^i ( F ` n ) ) )
52 48 51 eqtrd 
 |-  ( ph -> ( A i^i U_ n e. Z ( E ` n ) ) = U_ n e. Z ( A i^i ( F ` n ) ) )
53 52 fveq2d 
 |-  ( ph -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) = ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) )
54 53 14 eqeltrrd 
 |-  ( ph -> ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) e. RR )
55 43 54 eqeltrd 
 |-  ( ph -> ( O ` U_ n e. Z ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) e. RR )
56 1 3 7 37 55 9 omeiunltfirp 
 |-  ( ph -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) < ( sum_ n e. z ( O ` ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) + Y ) )
57 43 adantr 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( O ` U_ n e. Z ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) = ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) )
58 elpwinss 
 |-  ( z e. ( ~P Z i^i Fin ) -> z C_ Z )
59 58 adantr 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ n e. z ) -> z C_ Z )
60 simpr 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ n e. z ) -> n e. z )
61 59 60 sseldd 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ n e. z ) -> n e. Z )
62 61 adantll 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> n e. Z )
63 25 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( A i^i ( F ` n ) ) e. _V )
64 62 63 40 syl2anc 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) = ( A i^i ( F ` n ) ) )
65 64 fveq2d 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) = ( O ` ( A i^i ( F ` n ) ) ) )
66 65 sumeq2dv 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> sum_ n e. z ( O ` ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) = sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) )
67 66 oveq1d 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( sum_ n e. z ( O ` ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) + Y ) = ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
68 57 67 breq12d 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( ( O ` U_ n e. Z ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) < ( sum_ n e. z ( O ` ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) + Y ) <-> ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) )
69 68 biimpd 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( ( O ` U_ n e. Z ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) < ( sum_ n e. z ( O ` ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) + Y ) -> ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) )
70 69 reximdva 
 |-  ( ph -> ( E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) < ( sum_ n e. z ( O ` ( ( k e. Z |-> ( A i^i ( F ` k ) ) ) ` n ) ) + Y ) -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) )
71 56 70 mpd 
 |-  ( ph -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
72 6 adantr 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> M e. ZZ )
73 58 adantl 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> z C_ Z )
74 elinel2 
 |-  ( z e. ( ~P Z i^i Fin ) -> z e. Fin )
75 74 adantl 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> z e. Fin )
76 72 7 73 75 uzfissfz 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> E. k e. Z z C_ ( M ... k ) )
77 76 adantr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> E. k e. Z z C_ ( M ... k ) )
78 54 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) /\ z C_ ( M ... k ) ) -> ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) e. RR )
79 fzfid 
 |-  ( z C_ ( M ... k ) -> ( M ... k ) e. Fin )
80 id 
 |-  ( z C_ ( M ... k ) -> z C_ ( M ... k ) )
81 ssfi 
 |-  ( ( ( M ... k ) e. Fin /\ z C_ ( M ... k ) ) -> z e. Fin )
82 79 80 81 syl2anc 
 |-  ( z C_ ( M ... k ) -> z e. Fin )
83 82 adantl 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> z e. Fin )
84 1 ad2antrr 
 |-  ( ( ( ph /\ z C_ ( M ... k ) ) /\ n e. z ) -> O e. OutMeas )
85 4 ad2antrr 
 |-  ( ( ( ph /\ z C_ ( M ... k ) ) /\ n e. z ) -> A C_ X )
86 5 ad2antrr 
 |-  ( ( ( ph /\ z C_ ( M ... k ) ) /\ n e. z ) -> ( O ` A ) e. RR )
87 inss1 
 |-  ( A i^i ( F ` n ) ) C_ A
88 87 a1i 
 |-  ( ( ( ph /\ z C_ ( M ... k ) ) /\ n e. z ) -> ( A i^i ( F ` n ) ) C_ A )
89 84 3 85 86 88 omessre 
 |-  ( ( ( ph /\ z C_ ( M ... k ) ) /\ n e. z ) -> ( O ` ( A i^i ( F ` n ) ) ) e. RR )
90 83 89 fsumrecl 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) e. RR )
91 9 rpred 
 |-  ( ph -> Y e. RR )
92 91 adantr 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> Y e. RR )
93 90 92 readdcld 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) e. RR )
94 93 ad4ant14 
 |-  ( ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) /\ z C_ ( M ... k ) ) -> ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) e. RR )
95 fzfid 
 |-  ( ph -> ( M ... k ) e. Fin )
96 87 a1i 
 |-  ( ph -> ( A i^i ( F ` n ) ) C_ A )
97 1 3 4 5 96 omessre 
 |-  ( ph -> ( O ` ( A i^i ( F ` n ) ) ) e. RR )
98 97 adantr 
 |-  ( ( ph /\ n e. ( M ... k ) ) -> ( O ` ( A i^i ( F ` n ) ) ) e. RR )
99 95 98 fsumrecl 
 |-  ( ph -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) e. RR )
100 99 adantr 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) e. RR )
101 91 adantr 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> Y e. RR )
102 100 101 readdcld 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) e. RR )
103 102 ad2antrr 
 |-  ( ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) /\ z C_ ( M ... k ) ) -> ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) e. RR )
104 simplr 
 |-  ( ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) /\ z C_ ( M ... k ) ) -> ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
105 99 adantr 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) e. RR )
106 fzfid 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> ( M ... k ) e. Fin )
107 98 adantlr 
 |-  ( ( ( ph /\ z C_ ( M ... k ) ) /\ n e. ( M ... k ) ) -> ( O ` ( A i^i ( F ` n ) ) ) e. RR )
108 0xr 
 |-  0 e. RR*
109 108 a1i 
 |-  ( ( ph /\ n e. ( M ... k ) ) -> 0 e. RR* )
110 pnfxr 
 |-  +oo e. RR*
111 110 a1i 
 |-  ( ( ph /\ n e. ( M ... k ) ) -> +oo e. RR* )
112 1 3 20 omecl 
 |-  ( ph -> ( O ` ( A i^i ( F ` n ) ) ) e. ( 0 [,] +oo ) )
113 112 adantr 
 |-  ( ( ph /\ n e. ( M ... k ) ) -> ( O ` ( A i^i ( F ` n ) ) ) e. ( 0 [,] +oo ) )
114 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( O ` ( A i^i ( F ` n ) ) ) e. ( 0 [,] +oo ) ) -> 0 <_ ( O ` ( A i^i ( F ` n ) ) ) )
115 109 111 113 114 syl3anc 
 |-  ( ( ph /\ n e. ( M ... k ) ) -> 0 <_ ( O ` ( A i^i ( F ` n ) ) ) )
116 115 adantlr 
 |-  ( ( ( ph /\ z C_ ( M ... k ) ) /\ n e. ( M ... k ) ) -> 0 <_ ( O ` ( A i^i ( F ` n ) ) ) )
117 simpr 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> z C_ ( M ... k ) )
118 106 107 116 117 fsumless 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) <_ sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) )
119 90 105 92 118 leadd1dd 
 |-  ( ( ph /\ z C_ ( M ... k ) ) -> ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) <_ ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
120 119 ad4ant14 
 |-  ( ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) /\ z C_ ( M ... k ) ) -> ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) <_ ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
121 78 94 103 104 120 ltletrd 
 |-  ( ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) /\ z C_ ( M ... k ) ) -> ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
122 121 ex 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> ( z C_ ( M ... k ) -> ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) )
123 122 reximdv 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> ( E. k e. Z z C_ ( M ... k ) -> E. k e. Z ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) )
124 77 123 mpd 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> E. k e. Z ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
125 124 rexlimdva2 
 |-  ( ph -> ( E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. z ( O ` ( A i^i ( F ` n ) ) ) + Y ) -> E. k e. Z ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) )
126 71 125 mpd 
 |-  ( ph -> E. k e. Z ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
127 53 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) = ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) )
128 simpr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
129 127 128 eqbrtrd 
 |-  ( ( ( ph /\ k e. Z ) /\ ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
130 129 ex 
 |-  ( ( ph /\ k e. Z ) -> ( ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) )
131 130 reximdva 
 |-  ( ph -> ( E. k e. Z ( O ` U_ n e. Z ( A i^i ( F ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) -> E. k e. Z ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) )
132 126 131 mpd 
 |-  ( ph -> E. k e. Z ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
133 simpr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) )
134 1 adantr 
 |-  ( ( ph /\ k e. Z ) -> O e. OutMeas )
135 4 adantr 
 |-  ( ( ph /\ k e. Z ) -> A C_ X )
136 5 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( O ` A ) e. RR )
137 8 adantr 
 |-  ( ( ph /\ k e. Z ) -> E : Z --> S )
138 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
139 134 2 3 135 136 7 137 10 11 138 carageniuncllem1 
 |-  ( ( ph /\ k e. Z ) -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) )
140 139 oveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) = ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) )
141 140 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) = ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) )
142 133 141 breqtrd 
 |-  ( ( ( ph /\ k e. Z ) /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) )
143 142 ex 
 |-  ( ( ph /\ k e. Z ) -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) )
144 143 reximdva 
 |-  ( ph -> ( E. k e. Z ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) + Y ) -> E. k e. Z ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) )
145 132 144 mpd 
 |-  ( ph -> E. k e. Z ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) )
146 14 3ad2ant1 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) e. RR )
147 16 3ad2ant1 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) e. RR )
148 inss1 
 |-  ( A i^i ( G ` k ) ) C_ A
149 148 a1i 
 |-  ( ( ph /\ k e. Z ) -> ( A i^i ( G ` k ) ) C_ A )
150 134 3 135 136 149 omessre 
 |-  ( ( ph /\ k e. Z ) -> ( O ` ( A i^i ( G ` k ) ) ) e. RR )
151 91 adantr 
 |-  ( ( ph /\ k e. Z ) -> Y e. RR )
152 150 151 readdcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) e. RR )
153 152 3adant3 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) e. RR )
154 difssd 
 |-  ( ( ph /\ k e. Z ) -> ( A \ ( G ` k ) ) C_ A )
155 134 3 135 136 154 omessre 
 |-  ( ( ph /\ k e. Z ) -> ( O ` ( A \ ( G ` k ) ) ) e. RR )
156 155 3adant3 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( O ` ( A \ ( G ` k ) ) ) e. RR )
157 simp3 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) )
158 146 153 157 ltled 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) <_ ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) )
159 135 ssdifssd 
 |-  ( ( ph /\ k e. Z ) -> ( A \ ( G ` k ) ) C_ X )
160 oveq2 
 |-  ( n = k -> ( M ... n ) = ( M ... k ) )
161 160 iuneq1d 
 |-  ( n = k -> U_ i e. ( M ... n ) ( E ` i ) = U_ i e. ( M ... k ) ( E ` i ) )
162 ovex 
 |-  ( M ... k ) e. _V
163 fvex 
 |-  ( E ` i ) e. _V
164 162 163 iunex 
 |-  U_ i e. ( M ... k ) ( E ` i ) e. _V
165 161 10 164 fvmpt 
 |-  ( k e. Z -> ( G ` k ) = U_ i e. ( M ... k ) ( E ` i ) )
166 fveq2 
 |-  ( i = n -> ( E ` i ) = ( E ` n ) )
167 166 cbviunv 
 |-  U_ i e. ( M ... k ) ( E ` i ) = U_ n e. ( M ... k ) ( E ` n )
168 167 a1i 
 |-  ( k e. Z -> U_ i e. ( M ... k ) ( E ` i ) = U_ n e. ( M ... k ) ( E ` n ) )
169 165 168 eqtrd 
 |-  ( k e. Z -> ( G ` k ) = U_ n e. ( M ... k ) ( E ` n ) )
170 elfzuz 
 |-  ( i e. ( M ... k ) -> i e. ( ZZ>= ` M ) )
171 7 eqcomi 
 |-  ( ZZ>= ` M ) = Z
172 171 a1i 
 |-  ( i e. ( M ... k ) -> ( ZZ>= ` M ) = Z )
173 170 172 eleqtrd 
 |-  ( i e. ( M ... k ) -> i e. Z )
174 173 ssriv 
 |-  ( M ... k ) C_ Z
175 iunss1 
 |-  ( ( M ... k ) C_ Z -> U_ n e. ( M ... k ) ( E ` n ) C_ U_ n e. Z ( E ` n ) )
176 174 175 ax-mp 
 |-  U_ n e. ( M ... k ) ( E ` n ) C_ U_ n e. Z ( E ` n )
177 176 a1i 
 |-  ( k e. Z -> U_ n e. ( M ... k ) ( E ` n ) C_ U_ n e. Z ( E ` n ) )
178 169 177 eqsstrd 
 |-  ( k e. Z -> ( G ` k ) C_ U_ n e. Z ( E ` n ) )
179 178 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) C_ U_ n e. Z ( E ` n ) )
180 179 sscond 
 |-  ( ( ph /\ k e. Z ) -> ( A \ U_ n e. Z ( E ` n ) ) C_ ( A \ ( G ` k ) ) )
181 134 3 159 180 omessle 
 |-  ( ( ph /\ k e. Z ) -> ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) <_ ( O ` ( A \ ( G ` k ) ) ) )
182 181 3adant3 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) <_ ( O ` ( A \ ( G ` k ) ) ) )
183 146 147 153 156 158 182 le2addd 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) + ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) + ( O ` ( A \ ( G ` k ) ) ) ) )
184 150 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( O ` ( A i^i ( G ` k ) ) ) e. CC )
185 91 recnd 
 |-  ( ph -> Y e. CC )
186 185 adantr 
 |-  ( ( ph /\ k e. Z ) -> Y e. CC )
187 155 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( O ` ( A \ ( G ` k ) ) ) e. CC )
188 184 186 187 add32d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) + ( O ` ( A \ ( G ` k ) ) ) ) = ( ( ( O ` ( A i^i ( G ` k ) ) ) + ( O ` ( A \ ( G ` k ) ) ) ) + Y ) )
189 rexadd 
 |-  ( ( ( O ` ( A i^i ( G ` k ) ) ) e. RR /\ ( O ` ( A \ ( G ` k ) ) ) e. RR ) -> ( ( O ` ( A i^i ( G ` k ) ) ) +e ( O ` ( A \ ( G ` k ) ) ) ) = ( ( O ` ( A i^i ( G ` k ) ) ) + ( O ` ( A \ ( G ` k ) ) ) ) )
190 150 155 189 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> ( ( O ` ( A i^i ( G ` k ) ) ) +e ( O ` ( A \ ( G ` k ) ) ) ) = ( ( O ` ( A i^i ( G ` k ) ) ) + ( O ` ( A \ ( G ` k ) ) ) ) )
191 190 eqcomd 
 |-  ( ( ph /\ k e. Z ) -> ( ( O ` ( A i^i ( G ` k ) ) ) + ( O ` ( A \ ( G ` k ) ) ) ) = ( ( O ` ( A i^i ( G ` k ) ) ) +e ( O ` ( A \ ( G ` k ) ) ) ) )
192 nfv 
 |-  F/ i ph
193 8 adantr 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> E : Z --> S )
194 173 adantl 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> i e. Z )
195 193 194 ffvelcdmd 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> ( E ` i ) e. S )
196 192 1 2 95 195 caragenfiiuncl 
 |-  ( ph -> U_ i e. ( M ... k ) ( E ` i ) e. S )
197 196 adantr 
 |-  ( ( ph /\ k e. Z ) -> U_ i e. ( M ... k ) ( E ` i ) e. S )
198 10 161 138 197 fvmptd3 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = U_ i e. ( M ... k ) ( E ` i ) )
199 198 197 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. S )
200 134 2 3 199 135 caragensplit 
 |-  ( ( ph /\ k e. Z ) -> ( ( O ` ( A i^i ( G ` k ) ) ) +e ( O ` ( A \ ( G ` k ) ) ) ) = ( O ` A ) )
201 191 200 eqtrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( O ` ( A i^i ( G ` k ) ) ) + ( O ` ( A \ ( G ` k ) ) ) ) = ( O ` A ) )
202 201 oveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( O ` ( A i^i ( G ` k ) ) ) + ( O ` ( A \ ( G ` k ) ) ) ) + Y ) = ( ( O ` A ) + Y ) )
203 188 202 eqtrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) + ( O ` ( A \ ( G ` k ) ) ) ) = ( ( O ` A ) + Y ) )
204 203 3adant3 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) + ( O ` ( A \ ( G ` k ) ) ) ) = ( ( O ` A ) + Y ) )
205 183 204 breqtrd 
 |-  ( ( ph /\ k e. Z /\ ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) ) -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) + ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` A ) + Y ) )
206 205 3exp 
 |-  ( ph -> ( k e. Z -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) + ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` A ) + Y ) ) ) )
207 206 rexlimdv 
 |-  ( ph -> ( E. k e. Z ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) < ( ( O ` ( A i^i ( G ` k ) ) ) + Y ) -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) + ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` A ) + Y ) ) )
208 145 207 mpd 
 |-  ( ph -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) + ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` A ) + Y ) )
209 18 208 eqbrtrd 
 |-  ( ph -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` A ) + Y ) )