Metamath Proof Explorer

Theorem carsgclctunlem3

Description: Lemma for carsgclctun . (Contributed by Thierry Arnoux, 24-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 ) )
carsgsiga.3 
|- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
carsgclctun.1 
|- ( ph -> A ~<_ _om )
carsgclctun.2 
|- ( ph -> A C_ ( toCaraSiga ` M ) )
carsgclctunlem3.1 
|- ( ph -> E e. ~P O )
Assertion carsgclctunlem3 
|- ( ph -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )

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 carsgsiga.3 
 |-  ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
6 carsgclctun.1 
 |-  ( ph -> A ~<_ _om )
7 carsgclctun.2 
 |-  ( ph -> A C_ ( toCaraSiga ` M ) )
8 carsgclctunlem3.1 
 |-  ( ph -> E e. ~P O )
9 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
10 8 elpwincl1 
 |-  ( ph -> ( E i^i U. A ) e. ~P O )
11 2 10 ffvelcdmd 
 |-  ( ph -> ( M ` ( E i^i U. A ) ) e. ( 0 [,] +oo ) )
12 9 11 sselid 
 |-  ( ph -> ( M ` ( E i^i U. A ) ) e. RR* )
13 8 elpwdifcl 
 |-  ( ph -> ( E \ U. A ) e. ~P O )
14 2 13 ffvelcdmd 
 |-  ( ph -> ( M ` ( E \ U. A ) ) e. ( 0 [,] +oo ) )
15 9 14 sselid 
 |-  ( ph -> ( M ` ( E \ U. A ) ) e. RR* )
16 12 15 xaddcld 
 |-  ( ph -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* )
17 16 adantr 
 |-  ( ( ph /\ ( M ` E ) = +oo ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* )
18 pnfge 
 |-  ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ +oo )
19 17 18 syl 
 |-  ( ( ph /\ ( M ` E ) = +oo ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ +oo )
20 simpr 
 |-  ( ( ph /\ ( M ` E ) = +oo ) -> ( M ` E ) = +oo )
21 19 20 breqtrrd 
 |-  ( ( ph /\ ( M ` E ) = +oo ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
22 unieq 
 |-  ( A = (/) -> U. A = U. (/) )
23 uni0 
 |-  U. (/) = (/)
24 22 23 eqtrdi 
 |-  ( A = (/) -> U. A = (/) )
25 24 ineq2d 
 |-  ( A = (/) -> ( E i^i U. A ) = ( E i^i (/) ) )
26 in0 
 |-  ( E i^i (/) ) = (/)
27 25 26 eqtrdi 
 |-  ( A = (/) -> ( E i^i U. A ) = (/) )
28 27 fveq2d 
 |-  ( A = (/) -> ( M ` ( E i^i U. A ) ) = ( M ` (/) ) )
29 24 difeq2d 
 |-  ( A = (/) -> ( E \ U. A ) = ( E \ (/) ) )
30 dif0 
 |-  ( E \ (/) ) = E
31 29 30 eqtrdi 
 |-  ( A = (/) -> ( E \ U. A ) = E )
32 31 fveq2d 
 |-  ( A = (/) -> ( M ` ( E \ U. A ) ) = ( M ` E ) )
33 28 32 oveq12d 
 |-  ( A = (/) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( ( M ` (/) ) +e ( M ` E ) ) )
34 33 adantl 
 |-  ( ( ph /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( ( M ` (/) ) +e ( M ` E ) ) )
35 3 adantr 
 |-  ( ( ph /\ A = (/) ) -> ( M ` (/) ) = 0 )
36 35 oveq1d 
 |-  ( ( ph /\ A = (/) ) -> ( ( M ` (/) ) +e ( M ` E ) ) = ( 0 +e ( M ` E ) ) )
37 2 8 ffvelcdmd 
 |-  ( ph -> ( M ` E ) e. ( 0 [,] +oo ) )
38 9 37 sselid 
 |-  ( ph -> ( M ` E ) e. RR* )
39 38 adantr 
 |-  ( ( ph /\ A = (/) ) -> ( M ` E ) e. RR* )
40 xaddlid 
 |-  ( ( M ` E ) e. RR* -> ( 0 +e ( M ` E ) ) = ( M ` E ) )
41 39 40 syl 
 |-  ( ( ph /\ A = (/) ) -> ( 0 +e ( M ` E ) ) = ( M ` E ) )
42 34 36 41 3eqtrd 
 |-  ( ( ph /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( M ` E ) )
43 42 39 eqeltrd 
 |-  ( ( ph /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* )
44 xeqlelt 
 |-  ( ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* /\ ( M ` E ) e. RR* ) -> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( M ` E ) <-> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) /\ -. ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) < ( M ` E ) ) ) )
45 43 39 44 syl2anc 
 |-  ( ( ph /\ A = (/) ) -> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( M ` E ) <-> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) /\ -. ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) < ( M ` E ) ) ) )
46 42 45 mpbid 
 |-  ( ( ph /\ A = (/) ) -> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) /\ -. ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) < ( M ` E ) ) )
47 46 simpld 
 |-  ( ( ph /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
48 47 adantlr 
 |-  ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
49 fvex 
 |-  ( toCaraSiga ` M ) e. _V
50 49 ssex 
 |-  ( A C_ ( toCaraSiga ` M ) -> A e. _V )
51 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
52 7 50 51 3syl 
 |-  ( ph -> ( (/) ~< A <-> A =/= (/) ) )
53 52 biimpar 
 |-  ( ( ph /\ A =/= (/) ) -> (/) ~< A )
54 53 adantlr 
 |-  ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) -> (/) ~< A )
55 nnenom 
 |-  NN ~~ _om
56 55 ensymi 
 |-  _om ~~ NN
57 domentr 
 |-  ( ( A ~<_ _om /\ _om ~~ NN ) -> A ~<_ NN )
58 6 56 57 sylancl 
 |-  ( ph -> A ~<_ NN )
59 58 ad2antrr 
 |-  ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) -> A ~<_ NN )
60 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ NN ) -> E. f f : NN -onto-> A )
61 54 59 60 syl2anc 
 |-  ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) -> E. f f : NN -onto-> A )
62 fveq2 
 |-  ( n = k -> ( f ` n ) = ( f ` k ) )
63 62 iundisj 
 |-  U_ n e. NN ( f ` n ) = U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) )
64 fofn 
 |-  ( f : NN -onto-> A -> f Fn NN )
65 fniunfv 
 |-  ( f Fn NN -> U_ n e. NN ( f ` n ) = U. ran f )
66 64 65 syl 
 |-  ( f : NN -onto-> A -> U_ n e. NN ( f ` n ) = U. ran f )
67 forn 
 |-  ( f : NN -onto-> A -> ran f = A )
68 67 unieqd 
 |-  ( f : NN -onto-> A -> U. ran f = U. A )
69 66 68 eqtrd 
 |-  ( f : NN -onto-> A -> U_ n e. NN ( f ` n ) = U. A )
70 69 adantl 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> U_ n e. NN ( f ` n ) = U. A )
71 63 70 eqtr3id 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) = U. A )
72 71 ineq2d 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( E i^i U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) ) = ( E i^i U. A ) )
73 72 fveq2d 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( M ` ( E i^i U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) ) ) = ( M ` ( E i^i U. A ) ) )
74 71 difeq2d 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( E \ U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) ) = ( E \ U. A ) )
75 74 fveq2d 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( M ` ( E \ U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) ) ) = ( M ` ( E \ U. A ) ) )
76 73 75 oveq12d 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( ( M ` ( E i^i U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) ) ) +e ( M ` ( E \ U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) ) ) ) = ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) )
77 1 ad3antrrr 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> O e. V )
78 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> M : ~P O --> ( 0 [,] +oo ) )
79 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( M ` (/) ) = 0 )
80 4 3adant1r 
 |-  ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
81 80 3adant1r 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
82 81 3adant1r 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
83 5 3adant1r 
 |-  ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
84 83 3adant1r 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
85 84 3adant1r 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
86 62 iundisj2 
 |-  Disj_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) )
87 86 a1i 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> Disj_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) )
88 77 adantr 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> O e. V )
89 78 adantr 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
90 7 ad4antr 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> A C_ ( toCaraSiga ` M ) )
91 fof 
 |-  ( f : NN -onto-> A -> f : NN --> A )
92 91 ad2antlr 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> f : NN --> A )
93 simpr 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> n e. NN )
94 92 93 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( f ` n ) e. A )
95 90 94 sseldd 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( f ` n ) e. ( toCaraSiga ` M ) )
96 79 adantr 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( M ` (/) ) = 0 )
97 82 3adant1r 
 |-  ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
98 88 89 96 97 carsgsigalem 
 |-  ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ e e. ~P O /\ g e. ~P O ) -> ( M ` ( e u. g ) ) <_ ( ( M ` e ) +e ( M ` g ) ) )
99 91 ad3antlr 
 |-  ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> f : NN --> A )
100 fzossnn 
 |-  ( 1 ..^ n ) C_ NN
101 100 a1i 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( 1 ..^ n ) C_ NN )
102 101 sselda 
 |-  ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> k e. NN )
103 99 102 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> ( f ` k ) e. A )
104 103 ralrimiva 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> A. k e. ( 1 ..^ n ) ( f ` k ) e. A )
105 dfiun2g 
 |-  ( A. k e. ( 1 ..^ n ) ( f ` k ) e. A -> U_ k e. ( 1 ..^ n ) ( f ` k ) = U. { z | E. k e. ( 1 ..^ n ) z = ( f ` k ) } )
106 104 105 syl 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> U_ k e. ( 1 ..^ n ) ( f ` k ) = U. { z | E. k e. ( 1 ..^ n ) z = ( f ` k ) } )
107 eqid 
 |-  ( k e. ( 1 ..^ n ) |-> ( f ` k ) ) = ( k e. ( 1 ..^ n ) |-> ( f ` k ) )
108 107 rnmpt 
 |-  ran ( k e. ( 1 ..^ n ) |-> ( f ` k ) ) = { z | E. k e. ( 1 ..^ n ) z = ( f ` k ) }
109 fzofi 
 |-  ( 1 ..^ n ) e. Fin
110 mptfi 
 |-  ( ( 1 ..^ n ) e. Fin -> ( k e. ( 1 ..^ n ) |-> ( f ` k ) ) e. Fin )
111 rnfi 
 |-  ( ( k e. ( 1 ..^ n ) |-> ( f ` k ) ) e. Fin -> ran ( k e. ( 1 ..^ n ) |-> ( f ` k ) ) e. Fin )
112 109 110 111 mp2b 
 |-  ran ( k e. ( 1 ..^ n ) |-> ( f ` k ) ) e. Fin
113 108 112 eqeltrri 
 |-  { z | E. k e. ( 1 ..^ n ) z = ( f ` k ) } e. Fin
114 113 a1i 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> { z | E. k e. ( 1 ..^ n ) z = ( f ` k ) } e. Fin )
115 90 adantr 
 |-  ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> A C_ ( toCaraSiga ` M ) )
116 115 103 sseldd 
 |-  ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1 ..^ n ) ) -> ( f ` k ) e. ( toCaraSiga ` M ) )
117 116 ralrimiva 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> A. k e. ( 1 ..^ n ) ( f ` k ) e. ( toCaraSiga ` M ) )
118 107 rnmptss 
 |-  ( A. k e. ( 1 ..^ n ) ( f ` k ) e. ( toCaraSiga ` M ) -> ran ( k e. ( 1 ..^ n ) |-> ( f ` k ) ) C_ ( toCaraSiga ` M ) )
119 117 118 syl 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ran ( k e. ( 1 ..^ n ) |-> ( f ` k ) ) C_ ( toCaraSiga ` M ) )
120 108 119 eqsstrrid 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> { z | E. k e. ( 1 ..^ n ) z = ( f ` k ) } C_ ( toCaraSiga ` M ) )
121 88 89 96 97 114 120 fiunelcarsg 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> U. { z | E. k e. ( 1 ..^ n ) z = ( f ` k ) } e. ( toCaraSiga ` M ) )
122 106 121 eqeltrd 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> U_ k e. ( 1 ..^ n ) ( f ` k ) e. ( toCaraSiga ` M ) )
123 88 89 95 98 122 difelcarsg2 
 |-  ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) e. ( toCaraSiga ` M ) )
124 8 ad3antrrr 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> E e. ~P O )
125 simpllr 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( M ` E ) =/= +oo )
126 77 78 79 82 85 87 123 124 125 carsgclctunlem2 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( ( M ` ( E i^i U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) ) ) +e ( M ` ( E \ U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1 ..^ n ) ( f ` k ) ) ) ) ) <_ ( M ` E ) )
127 76 126 eqbrtrrd 
 |-  ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
128 61 127 exlimddv 
 |-  ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
129 48 128 pm2.61dane 
 |-  ( ( ph /\ ( M ` E ) =/= +oo ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
130 21 129 pm2.61dane 
 |-  ( ph -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )