Metamath Proof Explorer

Theorem isomenndlem

Description: O is sub-additive w.r.t. countable indexed union, implies that O is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of Fremlin1 p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses isomenndlem.o 
|- ( ph -> O : ~P X --> ( 0 [,] +oo ) )
isomenndlem.o0 
|- ( ph -> ( O ` (/) ) = 0 )
isomenndlem.y 
|- ( ph -> Y C_ ~P X )
isomenndlem.subadd 
|- ( ( ph /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) )
isomenndlem.b 
|- ( ph -> B C_ NN )
isomenndlem.f 
|- ( ph -> F : B -1-1-onto-> Y )
isomenndlem.a 
|- A = ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) )
Assertion isomenndlem 
|- ( ph -> ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) )

Proof

Step Hyp Ref Expression
1 isomenndlem.o 
 |-  ( ph -> O : ~P X --> ( 0 [,] +oo ) )
2 isomenndlem.o0 
 |-  ( ph -> ( O ` (/) ) = 0 )
3 isomenndlem.y 
 |-  ( ph -> Y C_ ~P X )
4 isomenndlem.subadd 
 |-  ( ( ph /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) )
5 isomenndlem.b 
 |-  ( ph -> B C_ NN )
6 isomenndlem.f 
 |-  ( ph -> F : B -1-1-onto-> Y )
7 isomenndlem.a 
 |-  A = ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) )
8 id 
 |-  ( ph -> ph )
9 iftrue 
 |-  ( n e. B -> if ( n e. B , ( F ` n ) , (/) ) = ( F ` n ) )
10 9 adantl 
 |-  ( ( ph /\ n e. B ) -> if ( n e. B , ( F ` n ) , (/) ) = ( F ` n ) )
11 f1of 
 |-  ( F : B -1-1-onto-> Y -> F : B --> Y )
12 6 11 syl 
 |-  ( ph -> F : B --> Y )
13 ssun1 
 |-  Y C_ ( Y u. { (/) } )
14 13 a1i 
 |-  ( ph -> Y C_ ( Y u. { (/) } ) )
15 12 14 fssd 
 |-  ( ph -> F : B --> ( Y u. { (/) } ) )
16 15 ffvelrnda 
 |-  ( ( ph /\ n e. B ) -> ( F ` n ) e. ( Y u. { (/) } ) )
17 10 16 eqeltrd 
 |-  ( ( ph /\ n e. B ) -> if ( n e. B , ( F ` n ) , (/) ) e. ( Y u. { (/) } ) )
18 17 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ n e. B ) -> if ( n e. B , ( F ` n ) , (/) ) e. ( Y u. { (/) } ) )
19 iffalse 
 |-  ( -. n e. B -> if ( n e. B , ( F ` n ) , (/) ) = (/) )
20 19 adantl 
 |-  ( ( ph /\ -. n e. B ) -> if ( n e. B , ( F ` n ) , (/) ) = (/) )
21 0ex 
 |-  (/) e. _V
22 21 snid 
 |-  (/) e. { (/) }
23 elun2 
 |-  ( (/) e. { (/) } -> (/) e. ( Y u. { (/) } ) )
24 22 23 ax-mp 
 |-  (/) e. ( Y u. { (/) } )
25 24 a1i 
 |-  ( ( ph /\ -. n e. B ) -> (/) e. ( Y u. { (/) } ) )
26 20 25 eqeltrd 
 |-  ( ( ph /\ -. n e. B ) -> if ( n e. B , ( F ` n ) , (/) ) e. ( Y u. { (/) } ) )
27 26 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ -. n e. B ) -> if ( n e. B , ( F ` n ) , (/) ) e. ( Y u. { (/) } ) )
28 18 27 pm2.61dan 
 |-  ( ( ph /\ n e. NN ) -> if ( n e. B , ( F ` n ) , (/) ) e. ( Y u. { (/) } ) )
29 28 7 fmptd 
 |-  ( ph -> A : NN --> ( Y u. { (/) } ) )
30 0elpw 
 |-  (/) e. ~P X
31 snssi 
 |-  ( (/) e. ~P X -> { (/) } C_ ~P X )
32 30 31 ax-mp 
 |-  { (/) } C_ ~P X
33 32 a1i 
 |-  ( ph -> { (/) } C_ ~P X )
34 3 33 unssd 
 |-  ( ph -> ( Y u. { (/) } ) C_ ~P X )
35 29 34 fssd 
 |-  ( ph -> A : NN --> ~P X )
36 nnex 
 |-  NN e. _V
37 36 mptex 
 |-  ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) e. _V
38 7 37 eqeltri 
 |-  A e. _V
39 feq1 
 |-  ( a = A -> ( a : NN --> ~P X <-> A : NN --> ~P X ) )
40 39 anbi2d 
 |-  ( a = A -> ( ( ph /\ a : NN --> ~P X ) <-> ( ph /\ A : NN --> ~P X ) ) )
41 fveq1 
 |-  ( a = A -> ( a ` n ) = ( A ` n ) )
42 41 iuneq2d 
 |-  ( a = A -> U_ n e. NN ( a ` n ) = U_ n e. NN ( A ` n ) )
43 42 fveq2d 
 |-  ( a = A -> ( O ` U_ n e. NN ( a ` n ) ) = ( O ` U_ n e. NN ( A ` n ) ) )
44 simpl 
 |-  ( ( a = A /\ n e. NN ) -> a = A )
45 44 fveq1d 
 |-  ( ( a = A /\ n e. NN ) -> ( a ` n ) = ( A ` n ) )
46 45 fveq2d 
 |-  ( ( a = A /\ n e. NN ) -> ( O ` ( a ` n ) ) = ( O ` ( A ` n ) ) )
47 46 mpteq2dva 
 |-  ( a = A -> ( n e. NN |-> ( O ` ( a ` n ) ) ) = ( n e. NN |-> ( O ` ( A ` n ) ) ) )
48 47 fveq2d 
 |-  ( a = A -> ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( A ` n ) ) ) ) )
49 43 48 breq12d 
 |-  ( a = A -> ( ( O ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) <-> ( O ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( A ` n ) ) ) ) ) )
50 40 49 imbi12d 
 |-  ( a = A -> ( ( ( ph /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) ) <-> ( ( ph /\ A : NN --> ~P X ) -> ( O ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( A ` n ) ) ) ) ) ) )
51 38 50 4 vtocl 
 |-  ( ( ph /\ A : NN --> ~P X ) -> ( O ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( A ` n ) ) ) ) )
52 8 35 51 syl2anc 
 |-  ( ph -> ( O ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( A ` n ) ) ) ) )
53 12 ad2antrr 
 |-  ( ( ( ph /\ B = NN ) /\ n e. NN ) -> F : B --> Y )
54 simpr 
 |-  ( ( B = NN /\ n e. NN ) -> n e. NN )
55 id 
 |-  ( B = NN -> B = NN )
56 55 eqcomd 
 |-  ( B = NN -> NN = B )
57 56 adantr 
 |-  ( ( B = NN /\ n e. NN ) -> NN = B )
58 54 57 eleqtrd 
 |-  ( ( B = NN /\ n e. NN ) -> n e. B )
59 58 adantll 
 |-  ( ( ( ph /\ B = NN ) /\ n e. NN ) -> n e. B )
60 53 59 ffvelrnd 
 |-  ( ( ( ph /\ B = NN ) /\ n e. NN ) -> ( F ` n ) e. Y )
61 eqid 
 |-  ( n e. NN |-> ( F ` n ) ) = ( n e. NN |-> ( F ` n ) )
62 60 61 fmptd 
 |-  ( ( ph /\ B = NN ) -> ( n e. NN |-> ( F ` n ) ) : NN --> Y )
63 7 a1i 
 |-  ( B = NN -> A = ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) )
64 58 iftrued 
 |-  ( ( B = NN /\ n e. NN ) -> if ( n e. B , ( F ` n ) , (/) ) = ( F ` n ) )
65 64 mpteq2dva 
 |-  ( B = NN -> ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) = ( n e. NN |-> ( F ` n ) ) )
66 63 65 eqtrd 
 |-  ( B = NN -> A = ( n e. NN |-> ( F ` n ) ) )
67 66 feq1d 
 |-  ( B = NN -> ( A : NN --> Y <-> ( n e. NN |-> ( F ` n ) ) : NN --> Y ) )
68 67 adantl 
 |-  ( ( ph /\ B = NN ) -> ( A : NN --> Y <-> ( n e. NN |-> ( F ` n ) ) : NN --> Y ) )
69 62 68 mpbird 
 |-  ( ( ph /\ B = NN ) -> A : NN --> Y )
70 f1ofo 
 |-  ( F : B -1-1-onto-> Y -> F : B -onto-> Y )
71 6 70 syl 
 |-  ( ph -> F : B -onto-> Y )
72 dffo3 
 |-  ( F : B -onto-> Y <-> ( F : B --> Y /\ A. y e. Y E. n e. B y = ( F ` n ) ) )
73 71 72 sylib 
 |-  ( ph -> ( F : B --> Y /\ A. y e. Y E. n e. B y = ( F ` n ) ) )
74 73 simprd 
 |-  ( ph -> A. y e. Y E. n e. B y = ( F ` n ) )
75 74 adantr 
 |-  ( ( ph /\ y e. Y ) -> A. y e. Y E. n e. B y = ( F ` n ) )
76 simpr 
 |-  ( ( ph /\ y e. Y ) -> y e. Y )
77 rspa 
 |-  ( ( A. y e. Y E. n e. B y = ( F ` n ) /\ y e. Y ) -> E. n e. B y = ( F ` n ) )
78 75 76 77 syl2anc 
 |-  ( ( ph /\ y e. Y ) -> E. n e. B y = ( F ` n ) )
79 78 adantlr 
 |-  ( ( ( ph /\ B = NN ) /\ y e. Y ) -> E. n e. B y = ( F ` n ) )
80 nfv 
 |-  F/ n ( ph /\ B = NN )
81 nfre1 
 |-  F/ n E. n e. NN y = ( A ` n )
82 simpr 
 |-  ( ( B = NN /\ n e. B ) -> n e. B )
83 simpl 
 |-  ( ( B = NN /\ n e. B ) -> B = NN )
84 82 83 eleqtrd 
 |-  ( ( B = NN /\ n e. B ) -> n e. NN )
85 84 adantll 
 |-  ( ( ( ph /\ B = NN ) /\ n e. B ) -> n e. NN )
86 85 3adant3 
 |-  ( ( ( ph /\ B = NN ) /\ n e. B /\ y = ( F ` n ) ) -> n e. NN )
87 63 fveq1d 
 |-  ( B = NN -> ( A ` n ) = ( ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) ` n ) )
88 87 3ad2ant1 
 |-  ( ( B = NN /\ n e. B /\ y = ( F ` n ) ) -> ( A ` n ) = ( ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) ` n ) )
89 fvex 
 |-  ( F ` n ) e. _V
90 89 21 ifex 
 |-  if ( n e. B , ( F ` n ) , (/) ) e. _V
91 90 a1i 
 |-  ( ( B = NN /\ n e. B ) -> if ( n e. B , ( F ` n ) , (/) ) e. _V )
92 eqid 
 |-  ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) = ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) )
93 92 fvmpt2 
 |-  ( ( n e. NN /\ if ( n e. B , ( F ` n ) , (/) ) e. _V ) -> ( ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) ` n ) = if ( n e. B , ( F ` n ) , (/) ) )
94 84 91 93 syl2anc 
 |-  ( ( B = NN /\ n e. B ) -> ( ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) ` n ) = if ( n e. B , ( F ` n ) , (/) ) )
95 9 adantl 
 |-  ( ( B = NN /\ n e. B ) -> if ( n e. B , ( F ` n ) , (/) ) = ( F ` n ) )
96 94 95 eqtrd 
 |-  ( ( B = NN /\ n e. B ) -> ( ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) ` n ) = ( F ` n ) )
97 96 3adant3 
 |-  ( ( B = NN /\ n e. B /\ y = ( F ` n ) ) -> ( ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) ) ` n ) = ( F ` n ) )
98 id 
 |-  ( y = ( F ` n ) -> y = ( F ` n ) )
99 98 eqcomd 
 |-  ( y = ( F ` n ) -> ( F ` n ) = y )
100 99 3ad2ant3 
 |-  ( ( B = NN /\ n e. B /\ y = ( F ` n ) ) -> ( F ` n ) = y )
101 88 97 100 3eqtrrd 
 |-  ( ( B = NN /\ n e. B /\ y = ( F ` n ) ) -> y = ( A ` n ) )
102 101 3adant1l 
 |-  ( ( ( ph /\ B = NN ) /\ n e. B /\ y = ( F ` n ) ) -> y = ( A ` n ) )
103 rspe 
 |-  ( ( n e. NN /\ y = ( A ` n ) ) -> E. n e. NN y = ( A ` n ) )
104 86 102 103 syl2anc 
 |-  ( ( ( ph /\ B = NN ) /\ n e. B /\ y = ( F ` n ) ) -> E. n e. NN y = ( A ` n ) )
105 104 3exp 
 |-  ( ( ph /\ B = NN ) -> ( n e. B -> ( y = ( F ` n ) -> E. n e. NN y = ( A ` n ) ) ) )
106 80 81 105 rexlimd 
 |-  ( ( ph /\ B = NN ) -> ( E. n e. B y = ( F ` n ) -> E. n e. NN y = ( A ` n ) ) )
107 106 adantr 
 |-  ( ( ( ph /\ B = NN ) /\ y e. Y ) -> ( E. n e. B y = ( F ` n ) -> E. n e. NN y = ( A ` n ) ) )
108 79 107 mpd 
 |-  ( ( ( ph /\ B = NN ) /\ y e. Y ) -> E. n e. NN y = ( A ` n ) )
109 108 ralrimiva 
 |-  ( ( ph /\ B = NN ) -> A. y e. Y E. n e. NN y = ( A ` n ) )
110 69 109 jca 
 |-  ( ( ph /\ B = NN ) -> ( A : NN --> Y /\ A. y e. Y E. n e. NN y = ( A ` n ) ) )
111 dffo3 
 |-  ( A : NN -onto-> Y <-> ( A : NN --> Y /\ A. y e. Y E. n e. NN y = ( A ` n ) ) )
112 110 111 sylibr 
 |-  ( ( ph /\ B = NN ) -> A : NN -onto-> Y )
113 founiiun 
 |-  ( A : NN -onto-> Y -> U. Y = U_ n e. NN ( A ` n ) )
114 112 113 syl 
 |-  ( ( ph /\ B = NN ) -> U. Y = U_ n e. NN ( A ` n ) )
115 uniun 
 |-  U. ( Y u. { (/) } ) = ( U. Y u. U. { (/) } )
116 21 unisn 
 |-  U. { (/) } = (/)
117 116 uneq2i 
 |-  ( U. Y u. U. { (/) } ) = ( U. Y u. (/) )
118 un0 
 |-  ( U. Y u. (/) ) = U. Y
119 115 117 118 3eqtrri 
 |-  U. Y = U. ( Y u. { (/) } )
120 119 a1i 
 |-  ( ( ph /\ -. B = NN ) -> U. Y = U. ( Y u. { (/) } ) )
121 29 adantr 
 |-  ( ( ph /\ -. B = NN ) -> A : NN --> ( Y u. { (/) } ) )
122 nfv 
 |-  F/ n ( ( ph /\ -. B = NN ) /\ y = (/) )
123 5 adantr 
 |-  ( ( ph /\ -. B = NN ) -> B C_ NN )
124 55 necon3bi 
 |-  ( -. B = NN -> B =/= NN )
125 124 adantl 
 |-  ( ( ph /\ -. B = NN ) -> B =/= NN )
126 123 125 jca 
 |-  ( ( ph /\ -. B = NN ) -> ( B C_ NN /\ B =/= NN ) )
127 df-pss 
 |-  ( B C. NN <-> ( B C_ NN /\ B =/= NN ) )
128 126 127 sylibr 
 |-  ( ( ph /\ -. B = NN ) -> B C. NN )
129 pssnel 
 |-  ( B C. NN -> E. n ( n e. NN /\ -. n e. B ) )
130 128 129 syl 
 |-  ( ( ph /\ -. B = NN ) -> E. n ( n e. NN /\ -. n e. B ) )
131 130 adantr 
 |-  ( ( ( ph /\ -. B = NN ) /\ y = (/) ) -> E. n ( n e. NN /\ -. n e. B ) )
132 simprl 
 |-  ( ( ( ph /\ y = (/) ) /\ ( n e. NN /\ -. n e. B ) ) -> n e. NN )
133 simprl 
 |-  ( ( ph /\ ( n e. NN /\ -. n e. B ) ) -> n e. NN )
134 90 a1i 
 |-  ( ( ph /\ ( n e. NN /\ -. n e. B ) ) -> if ( n e. B , ( F ` n ) , (/) ) e. _V )
135 7 fvmpt2 
 |-  ( ( n e. NN /\ if ( n e. B , ( F ` n ) , (/) ) e. _V ) -> ( A ` n ) = if ( n e. B , ( F ` n ) , (/) ) )
136 133 134 135 syl2anc 
 |-  ( ( ph /\ ( n e. NN /\ -. n e. B ) ) -> ( A ` n ) = if ( n e. B , ( F ` n ) , (/) ) )
137 136 adantlr 
 |-  ( ( ( ph /\ y = (/) ) /\ ( n e. NN /\ -. n e. B ) ) -> ( A ` n ) = if ( n e. B , ( F ` n ) , (/) ) )
138 19 ad2antll 
 |-  ( ( ( ph /\ y = (/) ) /\ ( n e. NN /\ -. n e. B ) ) -> if ( n e. B , ( F ` n ) , (/) ) = (/) )
139 id 
 |-  ( y = (/) -> y = (/) )
140 139 eqcomd 
 |-  ( y = (/) -> (/) = y )
141 140 ad2antlr 
 |-  ( ( ( ph /\ y = (/) ) /\ ( n e. NN /\ -. n e. B ) ) -> (/) = y )
142 137 138 141 3eqtrrd 
 |-  ( ( ( ph /\ y = (/) ) /\ ( n e. NN /\ -. n e. B ) ) -> y = ( A ` n ) )
143 132 142 103 syl2anc 
 |-  ( ( ( ph /\ y = (/) ) /\ ( n e. NN /\ -. n e. B ) ) -> E. n e. NN y = ( A ` n ) )
144 143 ex 
 |-  ( ( ph /\ y = (/) ) -> ( ( n e. NN /\ -. n e. B ) -> E. n e. NN y = ( A ` n ) ) )
145 144 adantlr 
 |-  ( ( ( ph /\ -. B = NN ) /\ y = (/) ) -> ( ( n e. NN /\ -. n e. B ) -> E. n e. NN y = ( A ` n ) ) )
146 122 81 131 145 exlimimdd 
 |-  ( ( ( ph /\ -. B = NN ) /\ y = (/) ) -> E. n e. NN y = ( A ` n ) )
147 146 adantlr 
 |-  ( ( ( ( ph /\ -. B = NN ) /\ y e. ( Y u. { (/) } ) ) /\ y = (/) ) -> E. n e. NN y = ( A ` n ) )
148 simplll 
 |-  ( ( ( ( ph /\ -. B = NN ) /\ y e. ( Y u. { (/) } ) ) /\ -. y = (/) ) -> ph )
149 simpl 
 |-  ( ( y e. ( Y u. { (/) } ) /\ -. y = (/) ) -> y e. ( Y u. { (/) } ) )
150 elsni 
 |-  ( y e. { (/) } -> y = (/) )
151 150 con3i 
 |-  ( -. y = (/) -> -. y e. { (/) } )
152 151 adantl 
 |-  ( ( y e. ( Y u. { (/) } ) /\ -. y = (/) ) -> -. y e. { (/) } )
153 elunnel2 
 |-  ( ( y e. ( Y u. { (/) } ) /\ -. y e. { (/) } ) -> y e. Y )
154 149 152 153 syl2anc 
 |-  ( ( y e. ( Y u. { (/) } ) /\ -. y = (/) ) -> y e. Y )
155 154 adantll 
 |-  ( ( ( ( ph /\ -. B = NN ) /\ y e. ( Y u. { (/) } ) ) /\ -. y = (/) ) -> y e. Y )
156 71 adantr 
 |-  ( ( ph /\ y e. Y ) -> F : B -onto-> Y )
157 foelrni 
 |-  ( ( F : B -onto-> Y /\ y e. Y ) -> E. n e. B ( F ` n ) = y )
158 156 76 157 syl2anc 
 |-  ( ( ph /\ y e. Y ) -> E. n e. B ( F ` n ) = y )
159 nfv 
 |-  F/ n ( ph /\ y e. Y )
160 5 sselda 
 |-  ( ( ph /\ n e. B ) -> n e. NN )
161 160 3adant3 
 |-  ( ( ph /\ n e. B /\ ( F ` n ) = y ) -> n e. NN )
162 160 90 135 sylancl 
 |-  ( ( ph /\ n e. B ) -> ( A ` n ) = if ( n e. B , ( F ` n ) , (/) ) )
163 162 10 eqtrd 
 |-  ( ( ph /\ n e. B ) -> ( A ` n ) = ( F ` n ) )
164 163 3adant3 
 |-  ( ( ph /\ n e. B /\ ( F ` n ) = y ) -> ( A ` n ) = ( F ` n ) )
165 simp3 
 |-  ( ( ph /\ n e. B /\ ( F ` n ) = y ) -> ( F ` n ) = y )
166 164 165 eqtr2d 
 |-  ( ( ph /\ n e. B /\ ( F ` n ) = y ) -> y = ( A ` n ) )
167 161 166 103 syl2anc 
 |-  ( ( ph /\ n e. B /\ ( F ` n ) = y ) -> E. n e. NN y = ( A ` n ) )
168 167 3exp 
 |-  ( ph -> ( n e. B -> ( ( F ` n ) = y -> E. n e. NN y = ( A ` n ) ) ) )
169 168 adantr 
 |-  ( ( ph /\ y e. Y ) -> ( n e. B -> ( ( F ` n ) = y -> E. n e. NN y = ( A ` n ) ) ) )
170 159 81 169 rexlimd 
 |-  ( ( ph /\ y e. Y ) -> ( E. n e. B ( F ` n ) = y -> E. n e. NN y = ( A ` n ) ) )
171 158 170 mpd 
 |-  ( ( ph /\ y e. Y ) -> E. n e. NN y = ( A ` n ) )
172 148 155 171 syl2anc 
 |-  ( ( ( ( ph /\ -. B = NN ) /\ y e. ( Y u. { (/) } ) ) /\ -. y = (/) ) -> E. n e. NN y = ( A ` n ) )
173 147 172 pm2.61dan 
 |-  ( ( ( ph /\ -. B = NN ) /\ y e. ( Y u. { (/) } ) ) -> E. n e. NN y = ( A ` n ) )
174 173 ralrimiva 
 |-  ( ( ph /\ -. B = NN ) -> A. y e. ( Y u. { (/) } ) E. n e. NN y = ( A ` n ) )
175 121 174 jca 
 |-  ( ( ph /\ -. B = NN ) -> ( A : NN --> ( Y u. { (/) } ) /\ A. y e. ( Y u. { (/) } ) E. n e. NN y = ( A ` n ) ) )
176 dffo3 
 |-  ( A : NN -onto-> ( Y u. { (/) } ) <-> ( A : NN --> ( Y u. { (/) } ) /\ A. y e. ( Y u. { (/) } ) E. n e. NN y = ( A ` n ) ) )
177 175 176 sylibr 
 |-  ( ( ph /\ -. B = NN ) -> A : NN -onto-> ( Y u. { (/) } ) )
178 founiiun 
 |-  ( A : NN -onto-> ( Y u. { (/) } ) -> U. ( Y u. { (/) } ) = U_ n e. NN ( A ` n ) )
179 177 178 syl 
 |-  ( ( ph /\ -. B = NN ) -> U. ( Y u. { (/) } ) = U_ n e. NN ( A ` n ) )
180 120 179 eqtrd 
 |-  ( ( ph /\ -. B = NN ) -> U. Y = U_ n e. NN ( A ` n ) )
181 114 180 pm2.61dan 
 |-  ( ph -> U. Y = U_ n e. NN ( A ` n ) )
182 181 fveq2d 
 |-  ( ph -> ( O ` U. Y ) = ( O ` U_ n e. NN ( A ` n ) ) )
183 uncom 
 |-  ( ( NN \ B ) u. B ) = ( B u. ( NN \ B ) )
184 183 a1i 
 |-  ( ph -> ( ( NN \ B ) u. B ) = ( B u. ( NN \ B ) ) )
185 undif 
 |-  ( B C_ NN <-> ( B u. ( NN \ B ) ) = NN )
186 5 185 sylib 
 |-  ( ph -> ( B u. ( NN \ B ) ) = NN )
187 184 186 eqtrd 
 |-  ( ph -> ( ( NN \ B ) u. B ) = NN )
188 187 eqcomd 
 |-  ( ph -> NN = ( ( NN \ B ) u. B ) )
189 188 mpteq1d 
 |-  ( ph -> ( n e. NN |-> ( O ` ( A ` n ) ) ) = ( n e. ( ( NN \ B ) u. B ) |-> ( O ` ( A ` n ) ) ) )
190 189 fveq2d 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( O ` ( A ` n ) ) ) ) = ( sum^ ` ( n e. ( ( NN \ B ) u. B ) |-> ( O ` ( A ` n ) ) ) ) )
191 nfv 
 |-  F/ n ph
192 difexg 
 |-  ( NN e. _V -> ( NN \ B ) e. _V )
193 36 192 ax-mp 
 |-  ( NN \ B ) e. _V
194 193 a1i 
 |-  ( ph -> ( NN \ B ) e. _V )
195 36 a1i 
 |-  ( ph -> NN e. _V )
196 195 5 ssexd 
 |-  ( ph -> B e. _V )
197 disjdifr 
 |-  ( ( NN \ B ) i^i B ) = (/)
198 197 a1i 
 |-  ( ph -> ( ( NN \ B ) i^i B ) = (/) )
199 simpl 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> ph )
200 eldifi 
 |-  ( n e. ( NN \ B ) -> n e. NN )
201 200 adantl 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> n e. NN )
202 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> O : ~P X --> ( 0 [,] +oo ) )
203 35 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. ~P X )
204 202 203 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( O ` ( A ` n ) ) e. ( 0 [,] +oo ) )
205 199 201 204 syl2anc 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> ( O ` ( A ` n ) ) e. ( 0 [,] +oo ) )
206 160 204 syldan 
 |-  ( ( ph /\ n e. B ) -> ( O ` ( A ` n ) ) e. ( 0 [,] +oo ) )
207 191 194 196 198 205 206 sge0splitmpt 
 |-  ( ph -> ( sum^ ` ( n e. ( ( NN \ B ) u. B ) |-> ( O ` ( A ` n ) ) ) ) = ( ( sum^ ` ( n e. ( NN \ B ) |-> ( O ` ( A ` n ) ) ) ) +e ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) ) )
208 eqid 
 |-  ( n e. B |-> ( O ` ( A ` n ) ) ) = ( n e. B |-> ( O ` ( A ` n ) ) )
209 206 208 fmptd 
 |-  ( ph -> ( n e. B |-> ( O ` ( A ` n ) ) ) : B --> ( 0 [,] +oo ) )
210 196 209 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) e. RR* )
211 210 xaddid2d 
 |-  ( ph -> ( 0 +e ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) ) = ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) )
212 90 a1i 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> if ( n e. B , ( F ` n ) , (/) ) e. _V )
213 201 212 135 syl2anc 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> ( A ` n ) = if ( n e. B , ( F ` n ) , (/) ) )
214 eldifn 
 |-  ( n e. ( NN \ B ) -> -. n e. B )
215 214 adantl 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> -. n e. B )
216 215 iffalsed 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> if ( n e. B , ( F ` n ) , (/) ) = (/) )
217 213 216 eqtrd 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> ( A ` n ) = (/) )
218 217 fveq2d 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> ( O ` ( A ` n ) ) = ( O ` (/) ) )
219 199 2 syl 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> ( O ` (/) ) = 0 )
220 218 219 eqtrd 
 |-  ( ( ph /\ n e. ( NN \ B ) ) -> ( O ` ( A ` n ) ) = 0 )
221 220 mpteq2dva 
 |-  ( ph -> ( n e. ( NN \ B ) |-> ( O ` ( A ` n ) ) ) = ( n e. ( NN \ B ) |-> 0 ) )
222 221 fveq2d 
 |-  ( ph -> ( sum^ ` ( n e. ( NN \ B ) |-> ( O ` ( A ` n ) ) ) ) = ( sum^ ` ( n e. ( NN \ B ) |-> 0 ) ) )
223 191 194 sge0z 
 |-  ( ph -> ( sum^ ` ( n e. ( NN \ B ) |-> 0 ) ) = 0 )
224 222 223 eqtrd 
 |-  ( ph -> ( sum^ ` ( n e. ( NN \ B ) |-> ( O ` ( A ` n ) ) ) ) = 0 )
225 224 oveq1d 
 |-  ( ph -> ( ( sum^ ` ( n e. ( NN \ B ) |-> ( O ` ( A ` n ) ) ) ) +e ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) ) = ( 0 +e ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) ) )
226 1 3 feqresmpt 
 |-  ( ph -> ( O |` Y ) = ( y e. Y |-> ( O ` y ) ) )
227 226 fveq2d 
 |-  ( ph -> ( sum^ ` ( O |` Y ) ) = ( sum^ ` ( y e. Y |-> ( O ` y ) ) ) )
228 nfv 
 |-  F/ y ph
229 fveq2 
 |-  ( y = ( A ` n ) -> ( O ` y ) = ( O ` ( A ` n ) ) )
230 163 eqcomd 
 |-  ( ( ph /\ n e. B ) -> ( F ` n ) = ( A ` n ) )
231 1 adantr 
 |-  ( ( ph /\ y e. Y ) -> O : ~P X --> ( 0 [,] +oo ) )
232 3 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. ~P X )
233 231 232 ffvelrnd 
 |-  ( ( ph /\ y e. Y ) -> ( O ` y ) e. ( 0 [,] +oo ) )
234 228 191 229 196 6 230 233 sge0f1o 
 |-  ( ph -> ( sum^ ` ( y e. Y |-> ( O ` y ) ) ) = ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) )
235 eqidd 
 |-  ( ph -> ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) = ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) )
236 227 234 235 3eqtrd 
 |-  ( ph -> ( sum^ ` ( O |` Y ) ) = ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) )
237 211 225 236 3eqtr4d 
 |-  ( ph -> ( ( sum^ ` ( n e. ( NN \ B ) |-> ( O ` ( A ` n ) ) ) ) +e ( sum^ ` ( n e. B |-> ( O ` ( A ` n ) ) ) ) ) = ( sum^ ` ( O |` Y ) ) )
238 190 207 237 3eqtrrd 
 |-  ( ph -> ( sum^ ` ( O |` Y ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( A ` n ) ) ) ) )
239 182 238 breq12d 
 |-  ( ph -> ( ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) <-> ( O ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( A ` n ) ) ) ) ) )
240 52 239 mpbird 
 |-  ( ph -> ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) )