Metamath Proof Explorer

Theorem omeiunltfirp

Description: If the outer measure of a countable union is not +oo , then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses omeiunltfirp.o 
|- ( ph -> O e. OutMeas )
omeiunltfirp.x 
|- X = U. dom O
omeiunltfirp.z 
|- Z = ( ZZ>= ` N )
omeiunltfirp.e 
|- ( ph -> E : Z --> ~P X )
omeiunltfirp.re 
|- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) e. RR )
omeiunltfirp.y 
|- ( ph -> Y e. RR+ )
Assertion omeiunltfirp 
|- ( ph -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )

Proof

Step Hyp Ref Expression
1 omeiunltfirp.o 
 |-  ( ph -> O e. OutMeas )
2 omeiunltfirp.x 
 |-  X = U. dom O
3 omeiunltfirp.z 
 |-  Z = ( ZZ>= ` N )
4 omeiunltfirp.e 
 |-  ( ph -> E : Z --> ~P X )
5 omeiunltfirp.re 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) e. RR )
6 omeiunltfirp.y 
 |-  ( ph -> Y e. RR+ )
7 3 fvexi 
 |-  Z e. _V
8 7 a1i 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> Z e. _V )
9 1 adantr 
 |-  ( ( ph /\ n e. Z ) -> O e. OutMeas )
10 4 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) e. ~P X )
11 fvex 
 |-  ( E ` n ) e. _V
12 11 elpw 
 |-  ( ( E ` n ) e. ~P X <-> ( E ` n ) C_ X )
13 10 12 sylib 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ X )
14 9 2 13 omecl 
 |-  ( ( ph /\ n e. Z ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
15 eqid 
 |-  ( n e. Z |-> ( O ` ( E ` n ) ) ) = ( n e. Z |-> ( O ` ( E ` n ) ) )
16 14 15 fmptd 
 |-  ( ph -> ( n e. Z |-> ( O ` ( E ` n ) ) ) : Z --> ( 0 [,] +oo ) )
17 16 adantr 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> ( n e. Z |-> ( O ` ( E ` n ) ) ) : Z --> ( 0 [,] +oo ) )
18 simpr 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo )
19 5 adantr 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> ( O ` U_ n e. Z ( E ` n ) ) e. RR )
20 8 17 18 19 sge0pnffigt 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) )
21 simpl 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) ) -> ( ph /\ z e. ( ~P Z i^i Fin ) ) )
22 simpr 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) )
23 elpwinss 
 |-  ( z e. ( ~P Z i^i Fin ) -> z C_ Z )
24 23 resmptd 
 |-  ( z e. ( ~P Z i^i Fin ) -> ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) = ( n e. z |-> ( O ` ( E ` n ) ) ) )
25 24 fveq2d 
 |-  ( z e. ( ~P Z i^i Fin ) -> ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) = ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) )
26 25 adantr 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) ) -> ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) = ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) )
27 22 26 breqtrd 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) )
28 27 adantll 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) )
29 5 rexrd 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) e. RR* )
30 29 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) ) -> ( O ` U_ n e. Z ( E ` n ) ) e. RR* )
31 simpr 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> z e. ( ~P Z i^i Fin ) )
32 1 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> O e. OutMeas )
33 4 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> E : Z --> ~P X )
34 23 adantr 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ n e. z ) -> z C_ Z )
35 simpr 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ n e. z ) -> n e. z )
36 34 35 sseldd 
 |-  ( ( z e. ( ~P Z i^i Fin ) /\ n e. z ) -> n e. Z )
37 36 adantll 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> n e. Z )
38 33 37 ffvelrnd 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( E ` n ) e. ~P X )
39 38 12 sylib 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( E ` n ) C_ X )
40 32 2 39 omecl 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
41 eqid 
 |-  ( n e. z |-> ( O ` ( E ` n ) ) ) = ( n e. z |-> ( O ` ( E ` n ) ) )
42 40 41 fmptd 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( n e. z |-> ( O ` ( E ` n ) ) ) : z --> ( 0 [,] +oo ) )
43 31 42 sge0xrcl 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) e. RR* )
44 43 adantr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) ) -> ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) e. RR* )
45 elinel2 
 |-  ( z e. ( ~P Z i^i Fin ) -> z e. Fin )
46 45 adantl 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> z e. Fin )
47 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
48 0xr 
 |-  0 e. RR*
49 48 a1i 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> 0 e. RR* )
50 pnfxr 
 |-  +oo e. RR*
51 50 a1i 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> +oo e. RR* )
52 32 2 39 omexrcl 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` ( E ` n ) ) e. RR* )
53 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) ) -> 0 <_ ( O ` ( E ` n ) ) )
54 49 51 40 53 syl3anc 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> 0 <_ ( O ` ( E ` n ) ) )
55 13 ralrimiva 
 |-  ( ph -> A. n e. Z ( E ` n ) C_ X )
56 iunss 
 |-  ( U_ n e. Z ( E ` n ) C_ X <-> A. n e. Z ( E ` n ) C_ X )
57 55 56 sylibr 
 |-  ( ph -> U_ n e. Z ( E ` n ) C_ X )
58 57 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> U_ n e. Z ( E ` n ) C_ X )
59 32 2 58 omexrcl 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` U_ n e. Z ( E ` n ) ) e. RR* )
60 ssiun2 
 |-  ( n e. Z -> ( E ` n ) C_ U_ n e. Z ( E ` n ) )
61 37 60 syl 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( E ` n ) C_ U_ n e. Z ( E ` n ) )
62 32 2 58 61 omessle 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` ( E ` n ) ) <_ ( O ` U_ n e. Z ( E ` n ) ) )
63 5 ltpnfd 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) < +oo )
64 63 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` U_ n e. Z ( E ` n ) ) < +oo )
65 52 59 51 62 64 xrlelttrd 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` ( E ` n ) ) < +oo )
66 49 51 52 54 65 elicod 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` ( E ` n ) ) e. ( 0 [,) +oo ) )
67 47 66 sselid 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` ( E ` n ) ) e. RR )
68 46 67 fsumrecl 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> sum_ n e. z ( O ` ( E ` n ) ) e. RR )
69 6 rpred 
 |-  ( ph -> Y e. RR )
70 69 adantr 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> Y e. RR )
71 68 70 readdcld 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) e. RR )
72 71 rexrd 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) e. RR* )
73 72 adantr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) ) -> ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) e. RR* )
74 simpr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) )
75 66 41 fmptd 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( n e. z |-> ( O ` ( E ` n ) ) ) : z --> ( 0 [,) +oo ) )
76 46 75 sge0fsum 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) = sum_ k e. z ( ( n e. z |-> ( O ` ( E ` n ) ) ) ` k ) )
77 eqidd 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ k e. z ) -> ( n e. z |-> ( O ` ( E ` n ) ) ) = ( n e. z |-> ( O ` ( E ` n ) ) ) )
78 2fveq3 
 |-  ( n = k -> ( O ` ( E ` n ) ) = ( O ` ( E ` k ) ) )
79 78 adantl 
 |-  ( ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ k e. z ) /\ n = k ) -> ( O ` ( E ` n ) ) = ( O ` ( E ` k ) ) )
80 simpr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ k e. z ) -> k e. z )
81 fvexd 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ k e. z ) -> ( O ` ( E ` k ) ) e. _V )
82 77 79 80 81 fvmptd 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ k e. z ) -> ( ( n e. z |-> ( O ` ( E ` n ) ) ) ` k ) = ( O ` ( E ` k ) ) )
83 82 sumeq2dv 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> sum_ k e. z ( ( n e. z |-> ( O ` ( E ` n ) ) ) ` k ) = sum_ k e. z ( O ` ( E ` k ) ) )
84 2fveq3 
 |-  ( k = n -> ( O ` ( E ` k ) ) = ( O ` ( E ` n ) ) )
85 84 cbvsumv 
 |-  sum_ k e. z ( O ` ( E ` k ) ) = sum_ n e. z ( O ` ( E ` n ) )
86 85 a1i 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> sum_ k e. z ( O ` ( E ` k ) ) = sum_ n e. z ( O ` ( E ` n ) ) )
87 76 83 86 3eqtrd 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) = sum_ n e. z ( O ` ( E ` n ) ) )
88 6 adantr 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> Y e. RR+ )
89 68 88 ltaddrpd 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> sum_ n e. z ( O ` ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
90 87 89 eqbrtrd 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
91 90 adantr 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) ) -> ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
92 30 44 73 74 91 xrlttrd 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
93 21 28 92 syl2anc 
 |-  ( ( ( ph /\ z e. ( ~P Z i^i Fin ) ) /\ ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
94 93 ex 
 |-  ( ( ph /\ z e. ( ~P Z i^i Fin ) ) -> ( ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) ) )
95 94 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) /\ z e. ( ~P Z i^i Fin ) ) -> ( ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) ) )
96 95 reximdva 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> ( E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum^ ` ( ( n e. Z |-> ( O ` ( E ` n ) ) ) |` z ) ) -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) ) )
97 20 96 mpd 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
98 simpl 
 |-  ( ( ph /\ -. ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> ph )
99 simpr 
 |-  ( ( ph /\ -. ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> -. ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo )
100 7 a1i 
 |-  ( ph -> Z e. _V )
101 100 16 sge0repnf 
 |-  ( ph -> ( ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR <-> -. ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) )
102 101 adantr 
 |-  ( ( ph /\ -. ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> ( ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR <-> -. ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) )
103 99 102 mpbird 
 |-  ( ( ph /\ -. ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR )
104 nfv 
 |-  F/ n ph
105 nfcv 
 |-  F/_ n sum^
106 nfmpt1 
 |-  F/_ n ( n e. Z |-> ( O ` ( E ` n ) ) )
107 105 106 nffv 
 |-  F/_ n ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) )
108 nfcv 
 |-  F/_ n RR
109 107 108 nfel 
 |-  F/ n ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR
110 104 109 nfan 
 |-  F/ n ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR )
111 7 a1i 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) -> Z e. _V )
112 14 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ n e. Z ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
113 6 adantr 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) -> Y e. RR+ )
114 simpr 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) -> ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR )
115 110 111 112 113 114 sge0ltfirpmpt 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) -> E. z e. ( ~P Z i^i Fin ) ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) )
116 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) ) -> ( O ` U_ n e. Z ( E ` n ) ) e. RR )
117 114 ad2antrr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) ) -> ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR )
118 71 ad4ant13 
 |-  ( ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) ) -> ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) e. RR )
119 nfcv 
 |-  F/_ n E
120 104 119 1 2 3 4 omeiunle 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )
121 120 ad3antrrr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) ) -> ( O ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )
122 simpr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) ) -> ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) )
123 simpll 
 |-  ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) -> ph )
124 2fveq3 
 |-  ( n = m -> ( O ` ( E ` n ) ) = ( O ` ( E ` m ) ) )
125 124 cbvmptv 
 |-  ( n e. Z |-> ( O ` ( E ` n ) ) ) = ( m e. Z |-> ( O ` ( E ` m ) ) )
126 125 fveq2i 
 |-  ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = ( sum^ ` ( m e. Z |-> ( O ` ( E ` m ) ) ) )
127 126 eleq1i 
 |-  ( ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR <-> ( sum^ ` ( m e. Z |-> ( O ` ( E ` m ) ) ) ) e. RR )
128 127 biimpi 
 |-  ( ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR -> ( sum^ ` ( m e. Z |-> ( O ` ( E ` m ) ) ) ) e. RR )
129 128 ad2antlr 
 |-  ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( m e. Z |-> ( O ` ( E ` m ) ) ) ) e. RR )
130 simpr 
 |-  ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) -> z e. ( ~P Z i^i Fin ) )
131 45 adantl 
 |-  ( ( ( ph /\ ( sum^ ` ( m e. Z |-> ( O ` ( E ` m ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) -> z e. Fin )
132 66 adantllr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( m e. Z |-> ( O ` ( E ` m ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ n e. z ) -> ( O ` ( E ` n ) ) e. ( 0 [,) +oo ) )
133 131 132 sge0fsummpt 
 |-  ( ( ( ph /\ ( sum^ ` ( m e. Z |-> ( O ` ( E ` m ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) = sum_ n e. z ( O ` ( E ` n ) ) )
134 123 129 130 133 syl21anc 
 |-  ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) = sum_ n e. z ( O ` ( E ` n ) ) )
135 134 oveq1d 
 |-  ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) -> ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) = ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
136 135 adantr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) ) -> ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) = ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
137 122 136 breqtrd 
 |-  ( ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) ) -> ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
138 116 117 118 121 137 lelttrd 
 |-  ( ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
139 138 ex 
 |-  ( ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) /\ z e. ( ~P Z i^i Fin ) ) -> ( ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) -> ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) ) )
140 139 reximdva 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) -> ( E. z e. ( ~P Z i^i Fin ) ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) < ( ( sum^ ` ( n e. z |-> ( O ` ( E ` n ) ) ) ) + Y ) -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) ) )
141 115 140 mpd 
 |-  ( ( ph /\ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR ) -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
142 98 103 141 syl2anc 
 |-  ( ( ph /\ -. ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) = +oo ) -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
143 97 142 pm2.61dan 
 |-  ( ph -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )