Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  carsggect Structured version   Unicode version

Theorem carsggect 29152
Description: The outer measure is countably superadditive on Caratheodory measurable sets. (Contributed by Thierry Arnoux, 31-May-2020.)
Hypotheses
Ref Expression
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 )  <_ Σ* 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
Ref Expression
carsggect  |-  ( ph  -> Σ* z  e.  A ( M `
 z )  <_ 
( M `  U. A ) )
Distinct variable groups:    x, A, y    x, M, y    x, O, y    ph, x, y   
z, A    z, M    z, O, x, y    ph, z
Allowed substitution hints:    V( x, y, z)

Proof of Theorem carsggect
Dummy variables  f 
k  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 carsggect.1 . . 3  |-  ( ph  ->  A  ~<_  om )
2 0ex 4554 . . . 4  |-  (/)  e.  _V
32a1i 11 . . 3  |-  ( ph  -> 
(/)  e.  _V )
4 carsggect.0 . . 3  |-  ( ph  ->  -.  (/)  e.  A )
5 padct 28307 . . 3  |-  ( ( A  ~<_  om  /\  (/)  e.  _V  /\ 
-.  (/)  e.  A )  ->  E. f ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )
61, 3, 4, 5syl3anc 1265 . 2  |-  ( ph  ->  E. f ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )
7 nfv 1752 . . . . 5  |-  F/ z ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )
8 simpr1 1012 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  f : NN --> ( A  u.  {
(/) } ) )
98feqmptd 5932 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  f  =  ( k  e.  NN  |->  ( f `  k ) ) )
109rneqd 5079 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  =  ran  ( k  e.  NN  |->  ( f `
 k ) ) )
117, 10esumeq1d 28858 . . . 4  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  f ( M `  z )  = Σ* z  e. 
ran  ( k  e.  NN  |->  ( f `  k ) ) ( M `  z ) )
12 fvex 5889 . . . . . . . . . 10  |-  (toCaraSiga `  M
)  e.  _V
1312a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (toCaraSiga `  M )  e.  _V )
14 carsggect.2 . . . . . . . . . . 11  |-  ( ph  ->  A  C_  (toCaraSiga `  M
) )
1514adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A  C_  (toCaraSiga `  M ) )
16 carsgval.1 . . . . . . . . . . . . 13  |-  ( ph  ->  O  e.  V )
1716adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  O  e.  V )
18 carsgval.2 . . . . . . . . . . . . 13  |-  ( ph  ->  M : ~P O --> ( 0 [,] +oo ) )
1918adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  M : ~P O --> ( 0 [,] +oo ) )
20 carsgsiga.1 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M `  (/) )  =  0 )
2120adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( M `  (/) )  =  0 )
2217, 19, 210elcarsg 29141 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (/)  e.  (toCaraSiga `  M ) )
2322snssd 4143 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  { (/) } 
C_  (toCaraSiga `  M ) )
2415, 23unssd 3643 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( A  u.  { (/) } ) 
C_  (toCaraSiga `  M ) )
2513, 24ssexd 4569 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( A  u.  { (/) } )  e.  _V )
2619adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ( A  u.  { (/)
} ) )  ->  M : ~P O --> ( 0 [,] +oo ) )
2716, 18carsgcl 29138 . . . . . . . . . . . . 13  |-  ( ph  ->  (toCaraSiga `  M )  C_  ~P O )
2814, 27sstrd 3475 . . . . . . . . . . . 12  |-  ( ph  ->  A  C_  ~P O
)
2928adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A  C_ 
~P O )
30 0elpw 4591 . . . . . . . . . . . . 13  |-  (/)  e.  ~P O
3130a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (/)  e.  ~P O )
3231snssd 4143 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  { (/) } 
C_  ~P O )
3329, 32unssd 3643 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( A  u.  { (/) } ) 
C_  ~P O )
3433sselda 3465 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ( A  u.  { (/)
} ) )  -> 
z  e.  ~P O
)
3526, 34ffvelrnd 6036 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ( A  u.  { (/)
} ) )  -> 
( M `  z
)  e.  ( 0 [,] +oo ) )
36 frn 5750 . . . . . . . . 9  |-  ( f : NN --> ( A  u.  { (/) } )  ->  ran  f  C_  ( A  u.  { (/) } ) )
378, 36syl 17 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  C_  ( A  u.  {
(/) } ) )
387, 25, 35, 37esummono 28877 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  f ( M `  z )  <_ Σ* z  e.  ( A  u.  { (/) } ) ( M `  z ) )
39 ctex 28292 . . . . . . . . . 10  |-  ( A  ~<_  om  ->  A  e.  _V )
401, 39syl 17 . . . . . . . . 9  |-  ( ph  ->  A  e.  _V )
4140adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A  e.  _V )
4213, 23ssexd 4569 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  { (/) }  e.  _V )
4319adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  A )  ->  M : ~P O --> ( 0 [,] +oo ) )
4429sselda 3465 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  A )  ->  z  e.  ~P O )
4543, 44ffvelrnd 6036 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  A )  ->  ( M `  z )  e.  ( 0 [,] +oo ) )
46 elsni 4022 . . . . . . . . . . 11  |-  ( z  e.  { (/) }  ->  z  =  (/) )
4746adantl 468 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  { (/) } )  -> 
z  =  (/) )
4847fveq2d 5883 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  { (/) } )  -> 
( M `  z
)  =  ( M `
 (/) ) )
4921adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  { (/) } )  -> 
( M `  (/) )  =  0 )
5048, 49eqtrd 2464 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  { (/) } )  -> 
( M `  z
)  =  0 )
5141, 42, 45, 50esumpad 28878 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ( A  u.  { (/) } ) ( M `  z )  = Σ* z  e.  A ( M `  z ) )
5238, 51breqtrd 4446 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  f ( M `  z )  <_ Σ* z  e.  A
( M `  z
) )
5337, 24sstrd 3475 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  C_  (toCaraSiga `  M ) )
54 ssexg 4568 . . . . . . . 8  |-  ( ( ran  f  C_  (toCaraSiga `  M )  /\  (toCaraSiga `  M )  e.  _V )  ->  ran  f  e.  _V )
5553, 12, 54sylancl 667 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  e.  _V )
5619adantr 467 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ran  f )  ->  M : ~P O --> ( 0 [,] +oo ) )
5737, 33sstrd 3475 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  C_  ~P O )
5857sselda 3465 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ran  f )  -> 
z  e.  ~P O
)
5956, 58ffvelrnd 6036 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ran  f )  -> 
( M `  z
)  e.  ( 0 [,] +oo ) )
60 simpr2 1013 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A  C_ 
ran  f )
617, 55, 59, 60esummono 28877 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  A
( M `  z
)  <_ Σ* z  e.  ran  f ( M `  z ) )
6252, 61jca 535 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (Σ* z  e.  ran  f ( M `
 z )  <_ Σ* z  e.  A ( M `  z )  /\ Σ* z  e.  A
( M `  z
)  <_ Σ* z  e.  ran  f ( M `  z ) ) )
63 iccssxr 11719 . . . . . . 7  |-  ( 0 [,] +oo )  C_  RR*
6459ralrimiva 2840 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A. z  e.  ran  f ( M `
 z )  e.  ( 0 [,] +oo ) )
65 nfcv 2585 . . . . . . . . 9  |-  F/_ z ran  f
6665esumcl 28853 . . . . . . . 8  |-  ( ( ran  f  e.  _V  /\ 
A. z  e.  ran  f ( M `  z )  e.  ( 0 [,] +oo )
)  -> Σ* z  e.  ran  f ( M `  z )  e.  ( 0 [,] +oo )
)
6755, 64, 66syl2anc 666 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  f ( M `  z )  e.  ( 0 [,] +oo )
)
6863, 67sseldi 3463 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  f ( M `  z )  e.  RR* )
6945ralrimiva 2840 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A. z  e.  A  ( M `  z )  e.  ( 0 [,] +oo )
)
70 nfcv 2585 . . . . . . . . 9  |-  F/_ z A
7170esumcl 28853 . . . . . . . 8  |-  ( ( A  e.  _V  /\  A. z  e.  A  ( M `  z )  e.  ( 0 [,] +oo ) )  -> Σ* z  e.  A
( M `  z
)  e.  ( 0 [,] +oo ) )
7241, 69, 71syl2anc 666 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  A
( M `  z
)  e.  ( 0 [,] +oo ) )
7363, 72sseldi 3463 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  A
( M `  z
)  e.  RR* )
74 xrletri3 11453 . . . . . 6  |-  ( (Σ* z  e.  ran  f ( M `  z )  e.  RR*  /\ Σ* z  e.  A
( M `  z
)  e.  RR* )  ->  (Σ* z  e.  ran  f
( M `  z
)  = Σ* z  e.  A
( M `  z
)  <->  (Σ* z  e.  ran  f
( M `  z
)  <_ Σ* z  e.  A
( M `  z
)  /\ Σ* z  e.  A
( M `  z
)  <_ Σ* z  e.  ran  f ( M `  z ) ) ) )
7568, 73, 74syl2anc 666 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (Σ* z  e.  ran  f ( M `
 z )  = Σ* z  e.  A ( M `
 z )  <->  (Σ* z  e. 
ran  f ( M `
 z )  <_ Σ* z  e.  A ( M `  z )  /\ Σ* z  e.  A
( M `  z
)  <_ Σ* z  e.  ran  f ( M `  z ) ) ) )
7662, 75mpbird 236 . . . 4  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  f ( M `  z )  = Σ* z  e.  A ( M `  z ) )
77 fveq2 5879 . . . . 5  |-  ( z  =  ( f `  k )  ->  ( M `  z )  =  ( M `  ( f `  k
) ) )
78 nnex 10617 . . . . . 6  |-  NN  e.  _V
7978a1i 11 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  NN  e.  _V )
8019adantr 467 . . . . . 6  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  M : ~P O --> ( 0 [,] +oo ) )
8133adantr 467 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  ( A  u.  { (/) } ) 
C_  ~P O )
828adantr 467 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  f : NN --> ( A  u.  {
(/) } ) )
83 simpr 463 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  k  e.  NN )
8482, 83ffvelrnd 6036 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  (
f `  k )  e.  ( A  u.  { (/)
} ) )
8581, 84sseldd 3466 . . . . . 6  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  (
f `  k )  e.  ~P O )
8680, 85ffvelrnd 6036 . . . . 5  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  ( M `  ( f `  k ) )  e.  ( 0 [,] +oo ) )
87 simpr 463 . . . . . . 7  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  k  e.  NN )  /\  (
f `  k )  =  (/) )  ->  (
f `  k )  =  (/) )
8887fveq2d 5883 . . . . . 6  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  k  e.  NN )  /\  (
f `  k )  =  (/) )  ->  ( M `  ( f `  k ) )  =  ( M `  (/) ) )
8921ad2antrr 731 . . . . . 6  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  k  e.  NN )  /\  (
f `  k )  =  (/) )  ->  ( M `  (/) )  =  0 )
9088, 89eqtrd 2464 . . . . 5  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  k  e.  NN )  /\  (
f `  k )  =  (/) )  ->  ( M `  ( f `  k ) )  =  0 )
91 cnvimass 5205 . . . . . . . 8  |-  ( `' f " A ) 
C_  dom  f
9291a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " A
)  C_  dom  f )
93 fdm 5748 . . . . . . . 8  |-  ( f : NN --> ( A  u.  { (/) } )  ->  dom  f  =  NN )
948, 93syl 17 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  dom  f  =  NN )
9592, 94sseqtrd 3501 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " A
)  C_  NN )
96 ffun 5746 . . . . . . . . . . 11  |-  ( f : NN --> ( A  u.  { (/) } )  ->  Fun  f )
978, 96syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  Fun  f )
9897adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( NN  \  ( `' f " A
) ) )  ->  Fun  f )
99 difpreima 6021 . . . . . . . . . . . . 13  |-  ( Fun  f  ->  ( `' f " ( ( A  u.  { (/) } ) 
\  A ) )  =  ( ( `' f " ( A  u.  { (/) } ) )  \  ( `' f " A ) ) )
1008, 96, 993syl 18 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " (
( A  u.  { (/)
} )  \  A
) )  =  ( ( `' f "
( A  u.  { (/)
} ) )  \ 
( `' f " A ) ) )
101 fimacnv 6025 . . . . . . . . . . . . . 14  |-  ( f : NN --> ( A  u.  { (/) } )  ->  ( `' f
" ( A  u.  {
(/) } ) )  =  NN )
1028, 101syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " ( A  u.  { (/) } ) )  =  NN )
103102difeq1d 3583 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (
( `' f "
( A  u.  { (/)
} ) )  \ 
( `' f " A ) )  =  ( NN  \  ( `' f " A
) ) )
104100, 103eqtrd 2464 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " (
( A  u.  { (/)
} )  \  A
) )  =  ( NN  \  ( `' f " A ) ) )
105 uncom 3611 . . . . . . . . . . . . . . . 16  |-  ( {
(/) }  u.  A
)  =  ( A  u.  { (/) } )
106105difeq1i 3580 . . . . . . . . . . . . . . 15  |-  ( ( { (/) }  u.  A
)  \  A )  =  ( ( A  u.  { (/) } ) 
\  A )
107 difun2 3876 . . . . . . . . . . . . . . 15  |-  ( ( { (/) }  u.  A
)  \  A )  =  ( { (/) } 
\  A )
108106, 107eqtr3i 2454 . . . . . . . . . . . . . 14  |-  ( ( A  u.  { (/) } )  \  A )  =  ( { (/) } 
\  A )
109 difss 3593 . . . . . . . . . . . . . 14  |-  ( {
(/) }  \  A ) 
C_  { (/) }
110108, 109eqsstri 3495 . . . . . . . . . . . . 13  |-  ( ( A  u.  { (/) } )  \  A ) 
C_  { (/) }
111110a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (
( A  u.  { (/)
} )  \  A
)  C_  { (/) } )
112 sspreima 28242 . . . . . . . . . . . 12  |-  ( ( Fun  f  /\  (
( A  u.  { (/)
} )  \  A
)  C_  { (/) } )  ->  ( `' f
" ( ( A  u.  { (/) } ) 
\  A ) ) 
C_  ( `' f
" { (/) } ) )
11397, 111, 112syl2anc 666 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " (
( A  u.  { (/)
} )  \  A
) )  C_  ( `' f " { (/)
} ) )
114104, 113eqsstr3d 3500 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( NN  \  ( `' f
" A ) ) 
C_  ( `' f
" { (/) } ) )
115114sselda 3465 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( NN  \  ( `' f " A
) ) )  -> 
k  e.  ( `' f " { (/) } ) )
116 fvimacnvi 6009 . . . . . . . . 9  |-  ( ( Fun  f  /\  k  e.  ( `' f " { (/) } ) )  ->  ( f `  k )  e.  { (/)
} )
11798, 115, 116syl2anc 666 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( NN  \  ( `' f " A
) ) )  -> 
( f `  k
)  e.  { (/) } )
118 elsni 4022 . . . . . . . 8  |-  ( ( f `  k )  e.  { (/) }  ->  ( f `  k )  =  (/) )
119117, 118syl 17 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( NN  \  ( `' f " A
) ) )  -> 
( f `  k
)  =  (/) )
120119ralrimiva 2840 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A. k  e.  ( NN  \  ( `' f " A
) ) ( f `
 k )  =  (/) )
121 carsggect.3 . . . . . . . 8  |-  ( ph  -> Disj  y  e.  A  y
)
122121adantr 467 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  y  e.  A  y )
123 simpr3 1014 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  Fun  ( `' f  |`  A ) )
124 fresf1o 28227 . . . . . . . . . 10  |-  ( ( Fun  f  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) )  ->  ( f  |`  ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> A )
12597, 60, 123, 124syl3anc 1265 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (
f  |`  ( `' f
" A ) ) : ( `' f
" A ) -1-1-onto-> A )
126 simpr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  y  =  ( ( f  |`  ( `' f " A ) ) `  k ) )  -> 
y  =  ( ( f  |`  ( `' f " A ) ) `
 k ) )
127125, 126disjrdx 28197 . . . . . . . 8  |-  ( (
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 ) )
128 fvres 5893 . . . . . . . . . 10  |-  ( k  e.  ( `' f
" A )  -> 
( ( f  |`  ( `' f " A
) ) `  k
)  =  ( f `
 k ) )
129128adantl 468 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( `' f " A ) )  -> 
( ( f  |`  ( `' f " A
) ) `  k
)  =  ( f `
 k ) )
130129disjeq2dv 4397 . . . . . . . 8  |-  ( (
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
) ) )
131127, 130bitr3d 259 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (Disj  y  e.  A  y  <-> Disj  k  e.  ( `' f " A
) ( f `  k ) ) )
132122, 131mpbid 214 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  k  e.  ( `' f " A ) ( f `
 k ) )
133 disjss3 4420 . . . . . . 7  |-  ( ( ( `' 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
) ) )
134133biimpa 487 . . . . . 6  |-  ( ( ( ( `' 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 )
)
13595, 120, 132, 134syl21anc 1264 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  k  e.  NN  ( f `  k ) )
13677, 79, 86, 85, 90, 135esumrnmpt2 28891 . . . 4  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  ( k  e.  NN  |->  ( f `  k
) ) ( M `
 z )  = Σ* k  e.  NN ( M `
 ( f `  k ) ) )
13711, 76, 1363eqtr3rd 2473 . . 3  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* k  e.  NN ( M `  ( f `
 k ) )  = Σ* z  e.  A ( M `  z ) )
138 uniiun 4350 . . . . . . 7  |-  U. A  =  U_ x  e.  A  x
13928sselda 3465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  ~P O )
14040, 139elpwiuncl 28151 . . . . . . 7  |-  ( ph  ->  U_ x  e.  A  x  e.  ~P O
)
141138, 140syl5eqel 2515 . . . . . 6  |-  ( ph  ->  U. A  e.  ~P O )
142141adantr 467 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  U. A  e.  ~P O )
14319, 142ffvelrnd 6036 . . . 4  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( M `  U. A )  e.  ( 0 [,] +oo ) )
144 carsgsiga.2 . . . . . . . . . 10  |-  ( (
ph  /\  x  ~<_  om  /\  x  C_  ~P O )  ->  ( M `  U. x )  <_ Σ* y  e.  x
( M `  y
) )
1451443adant1r 1258 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  x  ~<_  om  /\  x  C_  ~P O )  ->  ( M `  U. x )  <_ Σ* y  e.  x ( M `  y ) )
146 fveq2 5879 . . . . . . . . . 10  |-  ( y  =  z  ->  ( M `  y )  =  ( M `  z ) )
147 nfcv 2585 . . . . . . . . . 10  |-  F/_ z
x
148 nfcv 2585 . . . . . . . . . 10  |-  F/_ y
x
149 nfcv 2585 . . . . . . . . . 10  |-  F/_ z
( M `  y
)
150 nfcv 2585 . . . . . . . . . 10  |-  F/_ y
( M `  z
)
151146, 147, 148, 149, 150cbvesum 28865 . . . . . . . . 9  |- Σ* y  e.  x
( M `  y
)  = Σ* z  e.  x
( M `  z
)
152145, 151syl6breq 4461 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  x  ~<_  om  /\  x  C_  ~P O )  ->  ( M `  U. x )  <_ Σ* z  e.  x ( M `  z ) )
153 ffn 5744 . . . . . . . . . 10  |-  ( f : NN --> ( A  u.  { (/) } )  ->  f  Fn  NN )
154 fz1ssnn 11832 . . . . . . . . . . 11  |-  ( 1 ... n )  C_  NN
155 fnssres 5705 . . . . . . . . . . 11  |-  ( ( f  Fn  NN  /\  ( 1 ... n
)  C_  NN )  ->  ( f  |`  (
1 ... n ) )  Fn  ( 1 ... n ) )
156154, 155mpan2 676 . . . . . . . . . 10  |-  ( f  Fn  NN  ->  (
f  |`  ( 1 ... n ) )  Fn  ( 1 ... n
) )
1578, 153, 1563syl 18 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (
f  |`  ( 1 ... n ) )  Fn  ( 1 ... n
) )
158 fzfi 12186 . . . . . . . . . 10  |-  ( 1 ... n )  e. 
Fin
159 fnfi 7853 . . . . . . . . . 10  |-  ( ( ( f  |`  (
1 ... n ) )  Fn  ( 1 ... n )  /\  (
1 ... n )  e. 
Fin )  ->  (
f  |`  ( 1 ... n ) )  e. 
Fin )
160158, 159mpan2 676 . . . . . . . . 9  |-  ( ( f  |`  ( 1 ... n ) )  Fn  ( 1 ... n )  ->  (
f  |`  ( 1 ... n ) )  e. 
Fin )
161 rnfi 7861 . . . . . . . . 9  |-  ( ( f  |`  ( 1 ... n ) )  e.  Fin  ->  ran  ( f  |`  (
1 ... n ) )  e.  Fin )
162157, 160, 1613syl 18 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  ( f  |`  (
1 ... n ) )  e.  Fin )
163 resss 5145 . . . . . . . . . . 11  |-  ( f  |`  ( 1 ... n
) )  C_  f
164 rnss 5080 . . . . . . . . . . 11  |-  ( ( f  |`  ( 1 ... n ) ) 
C_  f  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  ran  f )
165163, 164ax-mp 5 . . . . . . . . . 10  |-  ran  (
f  |`  ( 1 ... n ) )  C_  ran  f
166165a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  ran  f )
167166, 53sstrd 3475 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  (toCaraSiga `  M ) )
168166, 37sstrd 3475 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  ( A  u.  {
(/) } ) )
169 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ z
y
170 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ y
z
171 id 23 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  y  =  z )
172169, 170, 171cbvdisj 4402 . . . . . . . . . . . 12  |-  (Disj  y  e.  A  y  <-> Disj  z  e.  A  z )
173 disjun0 28201 . . . . . . . . . . . 12  |-  (Disj  z  e.  A  z  -> Disj  z  e.  ( A  u.  { (/)
} ) z )
174172, 173sylbi 199 . . . . . . . . . . 11  |-  (Disj  y  e.  A  y  -> Disj  z  e.  ( A  u.  { (/)
} ) z )
175121, 174syl 17 . . . . . . . . . 10  |-  ( ph  -> Disj  z  e.  ( A  u.  { (/) } ) z )
176175adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  z  e.  ( A  u.  { (/)
} ) z )
177 disjss1 4398 . . . . . . . . 9  |-  ( ran  ( f  |`  (
1 ... n ) ) 
C_  ( A  u.  {
(/) } )  ->  (Disj  z  e.  ( A  u.  {
(/) } ) z  -> Disj  z  e.  ran  ( f  |`  ( 1 ... n
) ) z ) )
178168, 176, 177sylc 63 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  z  e. 
ran  ( f  |`  ( 1 ... n
) ) z )
179 pwidg 3993 . . . . . . . . 9  |-  ( O  e.  V  ->  O  e.  ~P O )
18017, 179syl 17 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  O  e.  ~P O )
18117, 19, 21, 152, 162, 167, 178, 180carsgclctunlem1 29151 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( M `  ( O  i^i  U. ran  ( f  |`  ( 1 ... n
) ) ) )  = Σ* z  e.  ran  (
f  |`  ( 1 ... n ) ) ( M `  ( O  i^i  z ) ) )
182181adantr 467 . . . . . 6  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ( M `  ( O  i^i  U. ran  ( f  |`  ( 1 ... n
) ) ) )  = Σ* z  e.  ran  (
f  |`  ( 1 ... n ) ) ( M `  ( O  i^i  z ) ) )
183168unissd 4241 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  U. ran  ( f  |`  (
1 ... n ) ) 
C_  U. ( A  u.  {
(/) } ) )
184 uniun 4236 . . . . . . . . . . . 12  |-  U. ( A  u.  { (/) } )  =  ( U. A  u.  U. { (/) } )
1852unisn 4232 . . . . . . . . . . . . 13  |-  U. { (/)
}  =  (/)
186185uneq2i 3618 . . . . . . . . . . . 12  |-  ( U. A  u.  U. { (/) } )  =  ( U. A  u.  (/) )
187 un0 3788 . . . . . . . . . . . 12  |-  ( U. A  u.  (/) )  = 
U. A
188184, 186, 1873eqtri 2456 . . . . . . . . . . 11  |-  U. ( A  u.  { (/) } )  =  U. A
189183, 188syl6sseq 3511 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  U. ran  ( f  |`  (
1 ... n ) ) 
C_  U. A )
190189adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  U. ran  ( f  |`  (
1 ... n ) ) 
C_  U. A )
191 uniss 4238 . . . . . . . . . . . 12  |-  ( A 
C_  ~P O  ->  U. A  C_ 
U. ~P O )
192 unipw 4669 . . . . . . . . . . . 12  |-  U. ~P O  =  O
193191, 192syl6sseq 3511 . . . . . . . . . . 11  |-  ( A 
C_  ~P O  ->  U. A  C_  O )
19428, 193syl 17 . . . . . . . . . 10  |-  ( ph  ->  U. A  C_  O
)
195194ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  U. A  C_  O )
196190, 195sstrd 3475 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  U. ran  ( f  |`  (
1 ... n ) ) 
C_  O )
197 dfss1 3668 . . . . . . . 8  |-  ( U. ran  ( f  |`  (
1 ... n ) ) 
C_  O  <->  ( O  i^i  U. ran  ( f  |`  ( 1 ... n
) ) )  = 
U. ran  ( f  |`  ( 1 ... n
) ) )
198196, 197sylib 200 . . . . . . 7  |-  ( ( ( 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 ) ) )
199198fveq2d 5883 . . . . . 6  |-  ( ( ( 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
) ) ) )
200 nfv 1752 . . . . . . . 8  |-  F/ z ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )
201168adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  ( A  u.  {
(/) } ) )
20228ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  A  C_ 
~P O )
20330a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  (/)  e.  ~P O )
204203snssd 4143 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  { (/) } 
C_  ~P O )
205202, 204unssd 3643 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ( A  u.  { (/) } ) 
C_  ~P O )
206201, 205sstrd 3475 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  ~P O )
207206sselda 3465 . . . . . . . . . . . 12  |-  ( ( ( ( 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
)
208207elpwid 3990 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )  /\  z  e.  ran  ( f  |`  ( 1 ... n
) ) )  -> 
z  C_  O )
209 dfss1 3668 . . . . . . . . . . 11  |-  ( z 
C_  O  <->  ( O  i^i  z )  =  z )
210208, 209sylib 200 . . . . . . . . . 10  |-  ( ( ( ( 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 )
211210fveq2d 5883 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
212211ralrimiva 2840 . . . . . . . 8  |-  ( ( ( 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
) )
213200, 212esumeq2d 28860 . . . . . . 7  |-  ( ( ( 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 ) )  = Σ* z  e.  ran  (
f  |`  ( 1 ... n ) ) ( M `  z ) )
2149reseq1d 5121 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (
f  |`  ( 1 ... n ) )  =  ( ( k  e.  NN  |->  ( f `  k ) )  |`  ( 1 ... n
) ) )
215214adantr 467 . . . . . . . . . . 11  |-  ( ( ( 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
) ) )
216 resmpt 5171 . . . . . . . . . . . 12  |-  ( ( 1 ... n ) 
C_  NN  ->  ( ( k  e.  NN  |->  ( f `  k ) )  |`  ( 1 ... n ) )  =  ( k  e.  ( 1 ... n
)  |->  ( f `  k ) ) )
217154, 216ax-mp 5 . . . . . . . . . . 11  |-  ( ( k  e.  NN  |->  ( f `  k ) )  |`  ( 1 ... n ) )  =  ( k  e.  ( 1 ... n
)  |->  ( f `  k ) )
218215, 217syl6eq 2480 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  (
f  |`  ( 1 ... n ) )  =  ( k  e.  ( 1 ... n ) 
|->  ( f `  k
) ) )
219218eqcomd 2431 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  (
k  e.  ( 1 ... n )  |->  ( f `  k ) )  =  ( f  |`  ( 1 ... n
) ) )
220219rneqd 5079 . . . . . . . 8  |-  ( ( ( 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 ) ) )
221200, 220esumeq1d 28858 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  -> Σ* z  e.  ran  ( k  e.  ( 1 ... n ) 
|->  ( f `  k
) ) ( M `
 z )  = Σ* z  e.  ran  ( f  |`  ( 1 ... n
) ) ( M `
 z ) )
222158a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  (
1 ... n )  e. 
Fin )
22319ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  M : ~P O --> ( 0 [,] +oo ) )
224154a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  (
1 ... n )  C_  NN )
225224sselda 3465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  k  e.  NN )
22685adantlr 720 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )  /\  k  e.  NN )  ->  (
f `  k )  e.  ~P O )
227225, 226syldan 473 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
f `  k )  e.  ~P O )
228223, 227ffvelrnd 6036 . . . . . . . 8  |-  ( ( ( ( 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 ) )
229 simpr 463 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  /\  (
f `  k )  =  (/) )  ->  (
f `  k )  =  (/) )
230229fveq2d 5883 . . . . . . . . 9  |-  ( ( ( ( ( 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 `  (/) ) )
23121ad3antrrr 735 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  /\  (
f `  k )  =  (/) )  ->  ( M `  (/) )  =  0 )
232230, 231eqtrd 2464 . . . . . . . 8  |-  ( ( ( ( ( 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 )
233 disjss1 4398 . . . . . . . . . . 11  |-  ( ( 1 ... n ) 
C_  NN  ->  (Disj  k  e.  NN  ( f `  k )  -> Disj  k  e.  ( 1 ... n
) ( f `  k ) ) )
234154, 233ax-mp 5 . . . . . . . . . 10  |-  (Disj  k  e.  NN  ( f `  k )  -> Disj  k  e.  ( 1 ... n
) ( f `  k ) )
235135, 234syl 17 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  k  e.  ( 1 ... n
) ( f `  k ) )
236235adantr 467 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  -> Disj  k  e.  ( 1 ... n
) ( f `  k ) )
23777, 222, 228, 227, 232, 236esumrnmpt2 28891 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  -> Σ* z  e.  ran  ( k  e.  ( 1 ... n ) 
|->  ( f `  k
) ) ( M `
 z )  = Σ* k  e.  ( 1 ... n ) ( M `
 ( f `  k ) ) )
238213, 221, 2373eqtr2d 2470 . . . . . 6  |-  ( ( ( 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 ) )  = Σ* k  e.  ( 1 ... n ) ( M `  ( f `
 k ) ) )
239182, 199, 2383eqtr3d 2472 . . . . 5  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ( M `  U. ran  (
f  |`  ( 1 ... n ) ) )  = Σ* k  e.  ( 1 ... n ) ( M `  ( f `
 k ) ) )
240 carsggect.4 . . . . . . . 8  |-  ( (
ph  /\  x  C_  y  /\  y  e.  ~P O )  ->  ( M `  x )  <_  ( M `  y
) )
2412403adant1r 1258 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  x  C_  y  /\  y  e. 
~P O )  -> 
( M `  x
)  <_  ( M `  y ) )
24217, 19, 189, 142, 241carsgmon 29148 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( M `  U. ran  (
f  |`  ( 1 ... n ) ) )  <_  ( M `  U. A ) )
243242adantr 467 . . . . 5  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ( M `  U. ran  (
f  |`  ( 1 ... n ) ) )  <_  ( M `  U. A ) )
244239, 243eqbrtrrd 4444 . . . 4  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  -> Σ* k  e.  ( 1 ... n ) ( M `  (
f `  k )
)  <_  ( M `  U. A ) )
245143, 86, 244esumgect 28913 . . 3  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* k  e.  NN ( M `  ( f `
 k ) )  <_  ( M `  U. A ) )
246137, 245eqbrtrrd 4444 . 2  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  A
( M `  z
)  <_  ( M `  U. A ) )
2476, 246exlimddv 1771 1  |-  ( ph  -> Σ* z  e.  A ( M `
 z )  <_ 
( M `  U. A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 983    = wceq 1438   E.wex 1660    e. wcel 1869   A.wral 2776   _Vcvv 3082    \ cdif 3434    u. cun 3435    i^i cin 3436    C_ wss 3437   (/)c0 3762   ~Pcpw 3980   {csn 3997   U.cuni 4217   U_ciun 4297  Disj wdisj 4392   class class class wbr 4421    |-> cmpt 4480   `'ccnv 4850   dom cdm 4851   ran crn 4852    |` cres 4853   "cima 4854   Fun wfun 5593    Fn wfn 5594   -->wf 5595   -1-1-onto->wf1o 5598   ` cfv 5599  (class class class)co 6303   omcom 6704    ~<_ cdom 7573   Fincfn 7575   0cc0 9541   1c1 9542   +oocpnf 9674   RR*cxr 9676    <_ cle 9678   NNcn 10611   [,]cicc 11640   ...cfz 11786  Σ*cesum 28850  toCaraSigaccarsg 29135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619  ax-addf 9620  ax-mulf 9621
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-iin 4300  df-disj 4393  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-se 4811  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-isom 5608  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-of 6543  df-om 6705  df-1st 6805  df-2nd 6806  df-supp 6924  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-2o 7189  df-oadd 7192  df-er 7369  df-map 7480  df-pm 7481  df-ixp 7529  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-fsupp 7888  df-fi 7929  df-sup 7960  df-inf 7961  df-oi 8029  df-card 8376  df-cda 8600  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-4 10672  df-5 10673  df-6 10674  df-7 10675  df-8 10676  df-9 10677  df-10 10678  df-n0 10872  df-z 10940  df-dec 11054  df-uz 11162  df-q 11267  df-rp 11305  df-xneg 11411  df-xadd 11412  df-xmul 11413  df-ioo 11641  df-ioc 11642  df-ico 11643  df-icc 11644  df-fz 11787  df-fzo 11918  df-fl 12029  df-mod 12098  df-seq 12215  df-exp 12274  df-fac 12461  df-bc 12489  df-hash 12517  df-shft 13124  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  df-limsup 13519  df-clim 13545  df-rlim 13546  df-sum 13746  df-ef 14114  df-sin 14116  df-cos 14117  df-pi 14119  df-struct 15116  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-mulr 15197  df-starv 15198  df-sca 15199  df-vsca 15200  df-ip 15201  df-tset 15202  df-ple 15203  df-ds 15205  df-unif 15206  df-hom 15207  df-cco 15208  df-rest 15314  df-topn 15315  df-0g 15333  df-gsum 15334  df-topgen 15335  df-pt 15336  df-prds 15339  df-ordt 15392  df-xrs 15393  df-qtop 15399  df-imas 15400  df-xps 15403  df-mre 15485  df-mrc 15486  df-acs 15488  df-ps 16439  df-tsr 16440  df-plusf 16480  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-mhm 16575  df-submnd 16576  df-grp 16666  df-minusg 16667  df-sbg 16668  df-mulg 16669  df-subg 16807  df-cntz 16964  df-cmn 17425  df-abl 17426  df-mgp 17717  df-ur 17729  df-ring 17775  df-cring 17776  df-subrg 17999  df-abv 18038  df-lmod 18086  df-scaf 18087  df-sra 18388  df-rgmod 18389  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-fbas 18960  df-fg 18961  df-cnfld 18964  df-top 19913  df-bases 19914  df-topon 19915  df-topsp 19916  df-cld 20026  df-ntr 20027  df-cls 20028  df-nei 20106  df-lp 20144  df-perf 20145  df-cn 20235  df-cnp 20236  df-haus 20323  df-tx 20569  df-hmeo 20762  df-fil 20853  df-fm 20945  df-flim 20946  df-flf 20947  df-tmd 21079  df-tgp 21080  df-tsms 21133  df-trg 21166  df-xms 21327  df-ms 21328  df-tms 21329  df-nm 21589  df-ngp 21590  df-nrg 21592  df-nlm 21593  df-ii 21901  df-cncf 21902  df-limc 22813  df-dv 22814  df-log 23498  df-esum 28851  df-carsg 29136
This theorem is referenced by:  omsmeas  29157  omsmeasOLD  29158
  Copyright terms: Public domain W3C validator