Metamath Proof Explorer

Theorem carsggect

Description: The outer measure is countably superadditive on Caratheodory measurable sets. (Contributed by Thierry Arnoux, 31-May-2020)

Ref Expression
Hypotheses carsgval.1 
|- ( ph -> O e. V )
carsgval.2 
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
carsgsiga.1 
|- ( ph -> ( M ` (/) ) = 0 )
carsgsiga.2 
|- ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
carsggect.0 
|- ( ph -> -. (/) e. A )
carsggect.1 
|- ( ph -> A ~<_ _om )
carsggect.2 
|- ( ph -> A C_ ( toCaraSiga ` M ) )
carsggect.3 
|- ( ph -> Disj_ y e. A y )
carsggect.4 
|- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
Assertion carsggect 
|- ( ph -> sum* z e. A ( M ` z ) <_ ( M ` U. A ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 
 |-  ( ph -> O e. V )
2 carsgval.2 
 |-  ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3 carsgsiga.1 
 |-  ( ph -> ( M ` (/) ) = 0 )
4 carsgsiga.2 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
5 carsggect.0 
 |-  ( ph -> -. (/) e. A )
6 carsggect.1 
 |-  ( ph -> A ~<_ _om )
7 carsggect.2 
 |-  ( ph -> A C_ ( toCaraSiga ` M ) )
8 carsggect.3 
 |-  ( ph -> Disj_ y e. A y )
9 carsggect.4 
 |-  ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
10 0ex 
 |-  (/) e. _V
11 10 a1i 
 |-  ( ph -> (/) e. _V )
12 padct 
 |-  ( ( A ~<_ _om /\ (/) e. _V /\ -. (/) e. A ) -> E. f ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
13 6 11 5 12 syl3anc 
 |-  ( ph -> E. f ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
14 nfv 
 |-  F/ z ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
15 simpr1 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> f : NN --> ( A u. { (/) } ) )
16 15 feqmptd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> f = ( k e. NN |-> ( f ` k ) ) )
17 16 rneqd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran f = ran ( k e. NN |-> ( f ` k ) ) )
18 14 17 esumeq1d 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. ran f ( M ` z ) = sum* z e. ran ( k e. NN |-> ( f ` k ) ) ( M ` z ) )
19 fvex 
 |-  ( toCaraSiga ` M ) e. _V
20 19 a1i 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( toCaraSiga ` M ) e. _V )
21 7 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> A C_ ( toCaraSiga ` M ) )
22 1 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> O e. V )
23 2 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> M : ~P O --> ( 0 [,] +oo ) )
24 3 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( M ` (/) ) = 0 )
25 22 23 24 0elcarsg 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> (/) e. ( toCaraSiga ` M ) )
26 25 snssd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> { (/) } C_ ( toCaraSiga ` M ) )
27 21 26 unssd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( A u. { (/) } ) C_ ( toCaraSiga ` M ) )
28 20 27 ssexd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( A u. { (/) } ) e. _V )
29 23 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. ( A u. { (/) } ) ) -> M : ~P O --> ( 0 [,] +oo ) )
30 1 2 carsgcl 
 |-  ( ph -> ( toCaraSiga ` M ) C_ ~P O )
31 7 30 sstrd 
 |-  ( ph -> A C_ ~P O )
32 31 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> A C_ ~P O )
33 0elpw 
 |-  (/) e. ~P O
34 33 a1i 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> (/) e. ~P O )
35 34 snssd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> { (/) } C_ ~P O )
36 32 35 unssd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( A u. { (/) } ) C_ ~P O )
37 36 sselda 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. ( A u. { (/) } ) ) -> z e. ~P O )
38 29 37 ffvelrnd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. ( A u. { (/) } ) ) -> ( M ` z ) e. ( 0 [,] +oo ) )
39 15 frnd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran f C_ ( A u. { (/) } ) )
40 14 28 38 39 esummono 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. ran f ( M ` z ) <_ sum* z e. ( A u. { (/) } ) ( M ` z ) )
41 ctex 
 |-  ( A ~<_ _om -> A e. _V )
42 6 41 syl 
 |-  ( ph -> A e. _V )
43 42 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> A e. _V )
44 20 26 ssexd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> { (/) } e. _V )
45 23 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. A ) -> M : ~P O --> ( 0 [,] +oo ) )
46 32 sselda 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. A ) -> z e. ~P O )
47 45 46 ffvelrnd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. A ) -> ( M ` z ) e. ( 0 [,] +oo ) )
48 elsni 
 |-  ( z e. { (/) } -> z = (/) )
49 48 adantl 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. { (/) } ) -> z = (/) )
50 49 fveq2d 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. { (/) } ) -> ( M ` z ) = ( M ` (/) ) )
51 24 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. { (/) } ) -> ( M ` (/) ) = 0 )
52 50 51 eqtrd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. { (/) } ) -> ( M ` z ) = 0 )
53 43 44 47 52 esumpad 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. ( A u. { (/) } ) ( M ` z ) = sum* z e. A ( M ` z ) )
54 40 53 breqtrd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. ran f ( M ` z ) <_ sum* z e. A ( M ` z ) )
55 39 27 sstrd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran f C_ ( toCaraSiga ` M ) )
56 ssexg 
 |-  ( ( ran f C_ ( toCaraSiga ` M ) /\ ( toCaraSiga ` M ) e. _V ) -> ran f e. _V )
57 55 19 56 sylancl 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran f e. _V )
58 23 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. ran f ) -> M : ~P O --> ( 0 [,] +oo ) )
59 39 36 sstrd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran f C_ ~P O )
60 59 sselda 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. ran f ) -> z e. ~P O )
61 58 60 ffvelrnd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ z e. ran f ) -> ( M ` z ) e. ( 0 [,] +oo ) )
62 simpr2 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> A C_ ran f )
63 14 57 61 62 esummono 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. A ( M ` z ) <_ sum* z e. ran f ( M ` z ) )
64 54 63 jca 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( sum* z e. ran f ( M ` z ) <_ sum* z e. A ( M ` z ) /\ sum* z e. A ( M ` z ) <_ sum* z e. ran f ( M ` z ) ) )
65 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
66 61 ralrimiva 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> A. z e. ran f ( M ` z ) e. ( 0 [,] +oo ) )
67 nfcv 
 |-  F/_ z ran f
68 67 esumcl 
 |-  ( ( ran f e. _V /\ A. z e. ran f ( M ` z ) e. ( 0 [,] +oo ) ) -> sum* z e. ran f ( M ` z ) e. ( 0 [,] +oo ) )
69 57 66 68 syl2anc 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. ran f ( M ` z ) e. ( 0 [,] +oo ) )
70 65 69 sseldi 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. ran f ( M ` z ) e. RR* )
71 47 ralrimiva 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> A. z e. A ( M ` z ) e. ( 0 [,] +oo ) )
72 nfcv 
 |-  F/_ z A
73 72 esumcl 
 |-  ( ( A e. _V /\ A. z e. A ( M ` z ) e. ( 0 [,] +oo ) ) -> sum* z e. A ( M ` z ) e. ( 0 [,] +oo ) )
74 43 71 73 syl2anc 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. A ( M ` z ) e. ( 0 [,] +oo ) )
75 65 74 sseldi 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. A ( M ` z ) e. RR* )
76 xrletri3 
 |-  ( ( sum* z e. ran f ( M ` z ) e. RR* /\ sum* z e. A ( M ` z ) e. RR* ) -> ( sum* z e. ran f ( M ` z ) = sum* z e. A ( M ` z ) <-> ( sum* z e. ran f ( M ` z ) <_ sum* z e. A ( M ` z ) /\ sum* z e. A ( M ` z ) <_ sum* z e. ran f ( M ` z ) ) ) )
77 70 75 76 syl2anc 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( sum* z e. ran f ( M ` z ) = sum* z e. A ( M ` z ) <-> ( sum* z e. ran f ( M ` z ) <_ sum* z e. A ( M ` z ) /\ sum* z e. A ( M ` z ) <_ sum* z e. ran f ( M ` z ) ) ) )
78 64 77 mpbird 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. ran f ( M ` z ) = sum* z e. A ( M ` z ) )
79 fveq2 
 |-  ( z = ( f ` k ) -> ( M ` z ) = ( M ` ( f ` k ) ) )
80 nnex 
 |-  NN e. _V
81 80 a1i 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> NN e. _V )
82 23 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
83 36 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) -> ( A u. { (/) } ) C_ ~P O )
84 15 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) -> f : NN --> ( A u. { (/) } ) )
85 simpr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) -> k e. NN )
86 84 85 ffvelrnd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) -> ( f ` k ) e. ( A u. { (/) } ) )
87 83 86 sseldd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) -> ( f ` k ) e. ~P O )
88 82 87 ffvelrnd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) -> ( M ` ( f ` k ) ) e. ( 0 [,] +oo ) )
89 simpr 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) /\ ( f ` k ) = (/) ) -> ( f ` k ) = (/) )
90 89 fveq2d 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) /\ ( f ` k ) = (/) ) -> ( M ` ( f ` k ) ) = ( M ` (/) ) )
91 24 ad2antrr 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) /\ ( f ` k ) = (/) ) -> ( M ` (/) ) = 0 )
92 90 91 eqtrd 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. NN ) /\ ( f ` k ) = (/) ) -> ( M ` ( f ` k ) ) = 0 )
93 cnvimass 
 |-  ( `' f " A ) C_ dom f
94 93 15 fssdm 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( `' f " A ) C_ NN )
95 ffun 
 |-  ( f : NN --> ( A u. { (/) } ) -> Fun f )
96 15 95 syl 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> Fun f )
97 96 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. ( NN \ ( `' f " A ) ) ) -> Fun f )
98 difpreima 
 |-  ( Fun f -> ( `' f " ( ( A u. { (/) } ) \ A ) ) = ( ( `' f " ( A u. { (/) } ) ) \ ( `' f " A ) ) )
99 15 95 98 3syl 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( `' f " ( ( A u. { (/) } ) \ A ) ) = ( ( `' f " ( A u. { (/) } ) ) \ ( `' f " A ) ) )
100 fimacnv 
 |-  ( f : NN --> ( A u. { (/) } ) -> ( `' f " ( A u. { (/) } ) ) = NN )
101 15 100 syl 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( `' f " ( A u. { (/) } ) ) = NN )
102 101 difeq1d 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( ( `' f " ( A u. { (/) } ) ) \ ( `' f " A ) ) = ( NN \ ( `' f " A ) ) )
103 99 102 eqtrd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( `' f " ( ( A u. { (/) } ) \ A ) ) = ( NN \ ( `' f " A ) ) )
104 uncom 
 |-  ( { (/) } u. A ) = ( A u. { (/) } )
105 104 difeq1i 
 |-  ( ( { (/) } u. A ) \ A ) = ( ( A u. { (/) } ) \ A )
106 difun2 
 |-  ( ( { (/) } u. A ) \ A ) = ( { (/) } \ A )
107 105 106 eqtr3i 
 |-  ( ( A u. { (/) } ) \ A ) = ( { (/) } \ A )
108 difss 
 |-  ( { (/) } \ A ) C_ { (/) }
109 107 108 eqsstri 
 |-  ( ( A u. { (/) } ) \ A ) C_ { (/) }
110 109 a1i 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( ( A u. { (/) } ) \ A ) C_ { (/) } )
111 sspreima 
 |-  ( ( Fun f /\ ( ( A u. { (/) } ) \ A ) C_ { (/) } ) -> ( `' f " ( ( A u. { (/) } ) \ A ) ) C_ ( `' f " { (/) } ) )
112 96 110 111 syl2anc 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( `' f " ( ( A u. { (/) } ) \ A ) ) C_ ( `' f " { (/) } ) )
113 103 112 eqsstrrd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( NN \ ( `' f " A ) ) C_ ( `' f " { (/) } ) )
114 113 sselda 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. ( NN \ ( `' f " A ) ) ) -> k e. ( `' f " { (/) } ) )
115 fvimacnvi 
 |-  ( ( Fun f /\ k e. ( `' f " { (/) } ) ) -> ( f ` k ) e. { (/) } )
116 97 114 115 syl2anc 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. ( NN \ ( `' f " A ) ) ) -> ( f ` k ) e. { (/) } )
117 elsni 
 |-  ( ( f ` k ) e. { (/) } -> ( f ` k ) = (/) )
118 116 117 syl 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. ( NN \ ( `' f " A ) ) ) -> ( f ` k ) = (/) )
119 118 ralrimiva 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> A. k e. ( NN \ ( `' f " A ) ) ( f ` k ) = (/) )
120 8 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> Disj_ y e. A y )
121 simpr3 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> Fun ( `' f |` A ) )
122 fresf1o 
 |-  ( ( Fun f /\ A C_ ran f /\ Fun ( `' f |` A ) ) -> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> A )
123 96 62 121 122 syl3anc 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> A )
124 simpr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ y = ( ( f |` ( `' f " A ) ) ` k ) ) -> y = ( ( f |` ( `' f " A ) ) ` k ) )
125 123 124 disjrdx 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( Disj_ k e. ( `' f " A ) ( ( f |` ( `' f " A ) ) ` k ) <-> Disj_ y e. A y ) )
126 fvres 
 |-  ( k e. ( `' f " A ) -> ( ( f |` ( `' f " A ) ) ` k ) = ( f ` k ) )
127 126 adantl 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ k e. ( `' f " A ) ) -> ( ( f |` ( `' f " A ) ) ` k ) = ( f ` k ) )
128 127 disjeq2dv 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( Disj_ k e. ( `' f " A ) ( ( f |` ( `' f " A ) ) ` k ) <-> Disj_ k e. ( `' f " A ) ( f ` k ) ) )
129 125 128 bitr3d 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( Disj_ y e. A y <-> Disj_ k e. ( `' f " A ) ( f ` k ) ) )
130 120 129 mpbid 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> Disj_ k e. ( `' f " A ) ( f ` k ) )
131 disjss3 
 |-  ( ( ( `' f " A ) C_ NN /\ A. k e. ( NN \ ( `' f " A ) ) ( f ` k ) = (/) ) -> ( Disj_ k e. ( `' f " A ) ( f ` k ) <-> Disj_ k e. NN ( f ` k ) ) )
132 131 biimpa 
 |-  ( ( ( ( `' f " A ) C_ NN /\ A. k e. ( NN \ ( `' f " A ) ) ( f ` k ) = (/) ) /\ Disj_ k e. ( `' f " A ) ( f ` k ) ) -> Disj_ k e. NN ( f ` k ) )
133 94 119 130 132 syl21anc 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> Disj_ k e. NN ( f ` k ) )
134 79 81 88 87 92 133 esumrnmpt2 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. ran ( k e. NN |-> ( f ` k ) ) ( M ` z ) = sum* k e. NN ( M ` ( f ` k ) ) )
135 18 78 134 3eqtr3rd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* k e. NN ( M ` ( f ` k ) ) = sum* z e. A ( M ` z ) )
136 uniiun 
 |-  U. A = U_ x e. A x
137 31 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. ~P O )
138 42 137 elpwiuncl 
 |-  ( ph -> U_ x e. A x e. ~P O )
139 136 138 eqeltrid 
 |-  ( ph -> U. A e. ~P O )
140 139 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> U. A e. ~P O )
141 23 140 ffvelrnd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( M ` U. A ) e. ( 0 [,] +oo ) )
142 4 3adant1r 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
143 fveq2 
 |-  ( y = z -> ( M ` y ) = ( M ` z ) )
144 nfcv 
 |-  F/_ z x
145 nfcv 
 |-  F/_ y x
146 nfcv 
 |-  F/_ z ( M ` y )
147 nfcv 
 |-  F/_ y ( M ` z )
148 143 144 145 146 147 cbvesum 
 |-  sum* y e. x ( M ` y ) = sum* z e. x ( M ` z )
149 142 148 breqtrdi 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* z e. x ( M ` z ) )
150 ffn 
 |-  ( f : NN --> ( A u. { (/) } ) -> f Fn NN )
151 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
152 fnssres 
 |-  ( ( f Fn NN /\ ( 1 ... n ) C_ NN ) -> ( f |` ( 1 ... n ) ) Fn ( 1 ... n ) )
153 151 152 mpan2 
 |-  ( f Fn NN -> ( f |` ( 1 ... n ) ) Fn ( 1 ... n ) )
154 15 150 153 3syl 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( f |` ( 1 ... n ) ) Fn ( 1 ... n ) )
155 fzfi 
 |-  ( 1 ... n ) e. Fin
156 fnfi 
 |-  ( ( ( f |` ( 1 ... n ) ) Fn ( 1 ... n ) /\ ( 1 ... n ) e. Fin ) -> ( f |` ( 1 ... n ) ) e. Fin )
157 155 156 mpan2 
 |-  ( ( f |` ( 1 ... n ) ) Fn ( 1 ... n ) -> ( f |` ( 1 ... n ) ) e. Fin )
158 rnfi 
 |-  ( ( f |` ( 1 ... n ) ) e. Fin -> ran ( f |` ( 1 ... n ) ) e. Fin )
159 154 157 158 3syl 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran ( f |` ( 1 ... n ) ) e. Fin )
160 resss 
 |-  ( f |` ( 1 ... n ) ) C_ f
161 rnss 
 |-  ( ( f |` ( 1 ... n ) ) C_ f -> ran ( f |` ( 1 ... n ) ) C_ ran f )
162 160 161 ax-mp 
 |-  ran ( f |` ( 1 ... n ) ) C_ ran f
163 162 a1i 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran ( f |` ( 1 ... n ) ) C_ ran f )
164 163 55 sstrd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran ( f |` ( 1 ... n ) ) C_ ( toCaraSiga ` M ) )
165 163 39 sstrd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ran ( f |` ( 1 ... n ) ) C_ ( A u. { (/) } ) )
166 nfcv 
 |-  F/_ z y
167 nfcv 
 |-  F/_ y z
168 id 
 |-  ( y = z -> y = z )
169 166 167 168 cbvdisj 
 |-  ( Disj_ y e. A y <-> Disj_ z e. A z )
170 disjun0 
 |-  ( Disj_ z e. A z -> Disj_ z e. ( A u. { (/) } ) z )
171 169 170 sylbi 
 |-  ( Disj_ y e. A y -> Disj_ z e. ( A u. { (/) } ) z )
172 8 171 syl 
 |-  ( ph -> Disj_ z e. ( A u. { (/) } ) z )
173 172 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> Disj_ z e. ( A u. { (/) } ) z )
174 disjss1 
 |-  ( ran ( f |` ( 1 ... n ) ) C_ ( A u. { (/) } ) -> ( Disj_ z e. ( A u. { (/) } ) z -> Disj_ z e. ran ( f |` ( 1 ... n ) ) z ) )
175 165 173 174 sylc 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> Disj_ z e. ran ( f |` ( 1 ... n ) ) z )
176 pwidg 
 |-  ( O e. V -> O e. ~P O )
177 22 176 syl 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> O e. ~P O )
178 22 23 24 149 159 164 175 177 carsgclctunlem1 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( M ` ( O i^i U. ran ( f |` ( 1 ... n ) ) ) ) = sum* z e. ran ( f |` ( 1 ... n ) ) ( M ` ( O i^i z ) ) )
179 178 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( M ` ( O i^i U. ran ( f |` ( 1 ... n ) ) ) ) = sum* z e. ran ( f |` ( 1 ... n ) ) ( M ` ( O i^i z ) ) )
180 165 unissd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> U. ran ( f |` ( 1 ... n ) ) C_ U. ( A u. { (/) } ) )
181 uniun 
 |-  U. ( A u. { (/) } ) = ( U. A u. U. { (/) } )
182 10 unisn 
 |-  U. { (/) } = (/)
183 182 uneq2i 
 |-  ( U. A u. U. { (/) } ) = ( U. A u. (/) )
184 un0 
 |-  ( U. A u. (/) ) = U. A
185 181 183 184 3eqtri 
 |-  U. ( A u. { (/) } ) = U. A
186 180 185 sseqtrdi 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> U. ran ( f |` ( 1 ... n ) ) C_ U. A )
187 186 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> U. ran ( f |` ( 1 ... n ) ) C_ U. A )
188 uniss 
 |-  ( A C_ ~P O -> U. A C_ U. ~P O )
189 unipw 
 |-  U. ~P O = O
190 188 189 sseqtrdi 
 |-  ( A C_ ~P O -> U. A C_ O )
191 31 190 syl 
 |-  ( ph -> U. A C_ O )
192 191 ad2antrr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> U. A C_ O )
193 187 192 sstrd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> U. ran ( f |` ( 1 ... n ) ) C_ O )
194 sseqin2 
 |-  ( U. ran ( f |` ( 1 ... n ) ) C_ O <-> ( O i^i U. ran ( f |` ( 1 ... n ) ) ) = U. ran ( f |` ( 1 ... n ) ) )
195 193 194 sylib 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( O i^i U. ran ( f |` ( 1 ... n ) ) ) = U. ran ( f |` ( 1 ... n ) ) )
196 195 fveq2d 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( M ` ( O i^i U. ran ( f |` ( 1 ... n ) ) ) ) = ( M ` U. ran ( f |` ( 1 ... n ) ) ) )
197 nfv 
 |-  F/ z ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN )
198 165 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ran ( f |` ( 1 ... n ) ) C_ ( A u. { (/) } ) )
199 31 ad2antrr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> A C_ ~P O )
200 33 a1i 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> (/) e. ~P O )
201 200 snssd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> { (/) } C_ ~P O )
202 199 201 unssd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( A u. { (/) } ) C_ ~P O )
203 198 202 sstrd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ran ( f |` ( 1 ... n ) ) C_ ~P O )
204 203 sselda 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ z e. ran ( f |` ( 1 ... n ) ) ) -> z e. ~P O )
205 204 elpwid 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ z e. ran ( f |` ( 1 ... n ) ) ) -> z C_ O )
206 sseqin2 
 |-  ( z C_ O <-> ( O i^i z ) = z )
207 205 206 sylib 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ z e. ran ( f |` ( 1 ... n ) ) ) -> ( O i^i z ) = z )
208 207 fveq2d 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ z e. ran ( f |` ( 1 ... n ) ) ) -> ( M ` ( O i^i z ) ) = ( M ` z ) )
209 208 ralrimiva 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> A. z e. ran ( f |` ( 1 ... n ) ) ( M ` ( O i^i z ) ) = ( M ` z ) )
210 197 209 esumeq2d 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> sum* z e. ran ( f |` ( 1 ... n ) ) ( M ` ( O i^i z ) ) = sum* z e. ran ( f |` ( 1 ... n ) ) ( M ` z ) )
211 16 reseq1d 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( f |` ( 1 ... n ) ) = ( ( k e. NN |-> ( f ` k ) ) |` ( 1 ... n ) ) )
212 211 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( f |` ( 1 ... n ) ) = ( ( k e. NN |-> ( f ` k ) ) |` ( 1 ... n ) ) )
213 resmpt 
 |-  ( ( 1 ... n ) C_ NN -> ( ( k e. NN |-> ( f ` k ) ) |` ( 1 ... n ) ) = ( k e. ( 1 ... n ) |-> ( f ` k ) ) )
214 151 213 ax-mp 
 |-  ( ( k e. NN |-> ( f ` k ) ) |` ( 1 ... n ) ) = ( k e. ( 1 ... n ) |-> ( f ` k ) )
215 212 214 eqtrdi 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( f |` ( 1 ... n ) ) = ( k e. ( 1 ... n ) |-> ( f ` k ) ) )
216 215 eqcomd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( k e. ( 1 ... n ) |-> ( f ` k ) ) = ( f |` ( 1 ... n ) ) )
217 216 rneqd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ran ( k e. ( 1 ... n ) |-> ( f ` k ) ) = ran ( f |` ( 1 ... n ) ) )
218 197 217 esumeq1d 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> sum* z e. ran ( k e. ( 1 ... n ) |-> ( f ` k ) ) ( M ` z ) = sum* z e. ran ( f |` ( 1 ... n ) ) ( M ` z ) )
219 155 a1i 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( 1 ... n ) e. Fin )
220 23 ad2antrr 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> M : ~P O --> ( 0 [,] +oo ) )
221 151 a1i 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( 1 ... n ) C_ NN )
222 221 sselda 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
223 87 adantlr 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. NN ) -> ( f ` k ) e. ~P O )
224 222 223 syldan 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( f ` k ) e. ~P O )
225 220 224 ffvelrnd 
 |-  ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( M ` ( f ` k ) ) e. ( 0 [,] +oo ) )
226 simpr 
 |-  ( ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ ( f ` k ) = (/) ) -> ( f ` k ) = (/) )
227 226 fveq2d 
 |-  ( ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ ( f ` k ) = (/) ) -> ( M ` ( f ` k ) ) = ( M ` (/) ) )
228 24 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ ( f ` k ) = (/) ) -> ( M ` (/) ) = 0 )
229 227 228 eqtrd 
 |-  ( ( ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ ( f ` k ) = (/) ) -> ( M ` ( f ` k ) ) = 0 )
230 disjss1 
 |-  ( ( 1 ... n ) C_ NN -> ( Disj_ k e. NN ( f ` k ) -> Disj_ k e. ( 1 ... n ) ( f ` k ) ) )
231 151 230 ax-mp 
 |-  ( Disj_ k e. NN ( f ` k ) -> Disj_ k e. ( 1 ... n ) ( f ` k ) )
232 133 231 syl 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> Disj_ k e. ( 1 ... n ) ( f ` k ) )
233 232 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> Disj_ k e. ( 1 ... n ) ( f ` k ) )
234 79 219 225 224 229 233 esumrnmpt2 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> sum* z e. ran ( k e. ( 1 ... n ) |-> ( f ` k ) ) ( M ` z ) = sum* k e. ( 1 ... n ) ( M ` ( f ` k ) ) )
235 210 218 234 3eqtr2d 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> sum* z e. ran ( f |` ( 1 ... n ) ) ( M ` ( O i^i z ) ) = sum* k e. ( 1 ... n ) ( M ` ( f ` k ) ) )
236 179 196 235 3eqtr3d 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( M ` U. ran ( f |` ( 1 ... n ) ) ) = sum* k e. ( 1 ... n ) ( M ` ( f ` k ) ) )
237 9 3adant1r 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
238 22 23 186 140 237 carsgmon 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> ( M ` U. ran ( f |` ( 1 ... n ) ) ) <_ ( M ` U. A ) )
239 238 adantr 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> ( M ` U. ran ( f |` ( 1 ... n ) ) ) <_ ( M ` U. A ) )
240 236 239 eqbrtrrd 
 |-  ( ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( M ` ( f ` k ) ) <_ ( M ` U. A ) )
241 141 88 240 esumgect 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* k e. NN ( M ` ( f ` k ) ) <_ ( M ` U. A ) )
242 135 241 eqbrtrrd 
 |-  ( ( ph /\ ( f : NN --> ( A u. { (/) } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) -> sum* z e. A ( M ` z ) <_ ( M ` U. A ) )
243 13 242 exlimddv 
 |-  ( ph -> sum* z e. A ( M ` z ) <_ ( M ` U. A ) )