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

Theorem carsggect 29198
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 4548 . . . 4  |-  (/)  e.  _V
32a1i 11 . . 3  |-  ( ph  -> 
(/)  e.  _V )
4 carsggect.0 . . 3  |-  ( ph  ->  -.  (/)  e.  A )
5 padct 28355 . . 3  |-  ( ( A  ~<_  om  /\  (/)  e.  _V  /\ 
-.  (/)  e.  A )  ->  E. f ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )
61, 3, 4, 5syl3anc 1276 . 2  |-  ( ph  ->  E. f ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )
7 nfv 1771 . . . . 5  |-  F/ z ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )
8 simpr1 1020 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  f : NN --> ( A  u.  {
(/) } ) )
98feqmptd 5940 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  f  =  ( k  e.  NN  |->  ( f `  k ) ) )
109rneqd 5080 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  =  ran  ( k  e.  NN  |->  ( f `
 k ) ) )
117, 10esumeq1d 28904 . . . 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 5897 . . . . . . . . . 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 471 . . . . . . . . . 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 471 . . . . . . . . . . . 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 471 . . . . . . . . . . . 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 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( M `  (/) )  =  0 )
2217, 19, 210elcarsg 29187 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (/)  e.  (toCaraSiga `  M ) )
2322snssd 4129 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  { (/) } 
C_  (toCaraSiga `  M ) )
2415, 23unssd 3621 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( A  u.  { (/) } ) 
C_  (toCaraSiga `  M ) )
2513, 24ssexd 4563 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( A  u.  { (/) } )  e.  _V )
2619adantr 471 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ( A  u.  { (/)
} ) )  ->  M : ~P O --> ( 0 [,] +oo ) )
2716, 18carsgcl 29184 . . . . . . . . . . . . 13  |-  ( ph  ->  (toCaraSiga `  M )  C_  ~P O )
2814, 27sstrd 3453 . . . . . . . . . . . 12  |-  ( ph  ->  A  C_  ~P O
)
2928adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A  C_ 
~P O )
30 0elpw 4585 . . . . . . . . . . . . 13  |-  (/)  e.  ~P O
3130a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (/)  e.  ~P O )
3231snssd 4129 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  { (/) } 
C_  ~P O )
3329, 32unssd 3621 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( A  u.  { (/) } ) 
C_  ~P O )
3433sselda 3443 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ( A  u.  { (/)
} ) )  -> 
z  e.  ~P O
)
3526, 34ffvelrnd 6045 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ( A  u.  { (/)
} ) )  -> 
( M `  z
)  e.  ( 0 [,] +oo ) )
36 frn 5757 . . . . . . . . 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 28923 . . . . . . 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 7609 . . . . . . . . . 10  |-  ( A  ~<_  om  ->  A  e.  _V )
401, 39syl 17 . . . . . . . . 9  |-  ( ph  ->  A  e.  _V )
4140adantr 471 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A  e.  _V )
4213, 23ssexd 4563 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  { (/) }  e.  _V )
4319adantr 471 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  A )  ->  M : ~P O --> ( 0 [,] +oo ) )
4429sselda 3443 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  A )  ->  z  e.  ~P O )
4543, 44ffvelrnd 6045 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  A )  ->  ( M `  z )  e.  ( 0 [,] +oo ) )
46 elsni 4004 . . . . . . . . . . 11  |-  ( z  e.  { (/) }  ->  z  =  (/) )
4746adantl 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  { (/) } )  -> 
z  =  (/) )
4847fveq2d 5891 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  { (/) } )  -> 
( M `  z
)  =  ( M `
 (/) ) )
4921adantr 471 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  { (/) } )  -> 
( M `  (/) )  =  0 )
5048, 49eqtrd 2495 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  { (/) } )  -> 
( M `  z
)  =  0 )
5141, 42, 45, 50esumpad 28924 . . . . . . 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 4440 . . . . . 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 3453 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  C_  (toCaraSiga `  M ) )
54 ssexg 4562 . . . . . . . 8  |-  ( ( ran  f  C_  (toCaraSiga `  M )  /\  (toCaraSiga `  M )  e.  _V )  ->  ran  f  e.  _V )
5553, 12, 54sylancl 673 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  e.  _V )
5619adantr 471 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ran  f )  ->  M : ~P O --> ( 0 [,] +oo ) )
5737, 33sstrd 3453 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  f  C_  ~P O )
5857sselda 3443 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ran  f )  -> 
z  e.  ~P O
)
5956, 58ffvelrnd 6045 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  z  e.  ran  f )  -> 
( M `  z
)  e.  ( 0 [,] +oo ) )
60 simpr2 1021 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A  C_ 
ran  f )
617, 55, 59, 60esummono 28923 . . . . . 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 539 . . . . 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 11745 . . . . . . 7  |-  ( 0 [,] +oo )  C_  RR*
6459ralrimiva 2813 . . . . . . . 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 2602 . . . . . . . . 9  |-  F/_ z ran  f
6665esumcl 28899 . . . . . . . 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 671 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  f ( M `  z )  e.  ( 0 [,] +oo )
)
6863, 67sseldi 3441 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  ran  f ( M `  z )  e.  RR* )
6945ralrimiva 2813 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  A. z  e.  A  ( M `  z )  e.  ( 0 [,] +oo )
)
70 nfcv 2602 . . . . . . . . 9  |-  F/_ z A
7170esumcl 28899 . . . . . . . 8  |-  ( ( A  e.  _V  /\  A. z  e.  A  ( M `  z )  e.  ( 0 [,] +oo ) )  -> Σ* z  e.  A
( M `  z
)  e.  ( 0 [,] +oo ) )
7241, 69, 71syl2anc 671 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  A
( M `  z
)  e.  ( 0 [,] +oo ) )
7363, 72sseldi 3441 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  A
( M `  z
)  e.  RR* )
74 xrletri3 11479 . . . . . 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 671 . . . . 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 240 . . . 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 5887 . . . . 5  |-  ( z  =  ( f `  k )  ->  ( M `  z )  =  ( M `  ( f `  k
) ) )
78 nnex 10642 . . . . . 6  |-  NN  e.  _V
7978a1i 11 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  NN  e.  _V )
8019adantr 471 . . . . . 6  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  M : ~P O --> ( 0 [,] +oo ) )
8133adantr 471 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  ( A  u.  { (/) } ) 
C_  ~P O )
828adantr 471 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  f : NN --> ( A  u.  {
(/) } ) )
83 simpr 467 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  k  e.  NN )
8482, 83ffvelrnd 6045 . . . . . . 7  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  (
f `  k )  e.  ( A  u.  { (/)
} ) )
8581, 84sseldd 3444 . . . . . 6  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  (
f `  k )  e.  ~P O )
8680, 85ffvelrnd 6045 . . . . 5  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  NN )  ->  ( M `  ( f `  k ) )  e.  ( 0 [,] +oo ) )
87 simpr 467 . . . . . . 7  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  k  e.  NN )  /\  (
f `  k )  =  (/) )  ->  (
f `  k )  =  (/) )
8887fveq2d 5891 . . . . . 6  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  k  e.  NN )  /\  (
f `  k )  =  (/) )  ->  ( M `  ( f `  k ) )  =  ( M `  (/) ) )
8921ad2antrr 737 . . . . . 6  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  k  e.  NN )  /\  (
f `  k )  =  (/) )  ->  ( M `  (/) )  =  0 )
9088, 89eqtrd 2495 . . . . 5  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  k  e.  NN )  /\  (
f `  k )  =  (/) )  ->  ( M `  ( f `  k ) )  =  0 )
91 cnvimass 5206 . . . . . . . 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 5755 . . . . . . . 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 3479 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " A
)  C_  NN )
96 ffun 5753 . . . . . . . . . . 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 471 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( NN  \  ( `' f " A
) ) )  ->  Fun  f )
99 difpreima 6030 . . . . . . . . . . . . 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 6034 . . . . . . . . . . . . . 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 3561 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (
( `' f "
( A  u.  { (/)
} ) )  \ 
( `' f " A ) )  =  ( NN  \  ( `' f " A
) ) )
104100, 103eqtrd 2495 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " (
( A  u.  { (/)
} )  \  A
) )  =  ( NN  \  ( `' f " A ) ) )
105 uncom 3589 . . . . . . . . . . . . . . . 16  |-  ( {
(/) }  u.  A
)  =  ( A  u.  { (/) } )
106105difeq1i 3558 . . . . . . . . . . . . . . 15  |-  ( ( { (/) }  u.  A
)  \  A )  =  ( ( A  u.  { (/) } ) 
\  A )
107 difun2 3858 . . . . . . . . . . . . . . 15  |-  ( ( { (/) }  u.  A
)  \  A )  =  ( { (/) } 
\  A )
108106, 107eqtr3i 2485 . . . . . . . . . . . . . 14  |-  ( ( A  u.  { (/) } )  \  A )  =  ( { (/) } 
\  A )
109 difss 3571 . . . . . . . . . . . . . 14  |-  ( {
(/) }  \  A ) 
C_  { (/) }
110108, 109eqsstri 3473 . . . . . . . . . . . . 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 28294 . . . . . . . . . . . 12  |-  ( ( Fun  f  /\  (
( A  u.  { (/)
} )  \  A
)  C_  { (/) } )  ->  ( `' f
" ( ( A  u.  { (/) } ) 
\  A ) ) 
C_  ( `' f
" { (/) } ) )
11397, 111, 112syl2anc 671 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( `' f " (
( A  u.  { (/)
} )  \  A
) )  C_  ( `' f " { (/)
} ) )
114104, 113eqsstr3d 3478 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( NN  \  ( `' f
" A ) ) 
C_  ( `' f
" { (/) } ) )
115114sselda 3443 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( NN  \  ( `' f " A
) ) )  -> 
k  e.  ( `' f " { (/) } ) )
116 fvimacnvi 6018 . . . . . . . . 9  |-  ( ( Fun  f  /\  k  e.  ( `' f " { (/) } ) )  ->  ( f `  k )  e.  { (/)
} )
11798, 115, 116syl2anc 671 . . . . . . . 8  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( NN  \  ( `' f " A
) ) )  -> 
( f `  k
)  e.  { (/) } )
118 elsni 4004 . . . . . . . 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 2813 . . . . . 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 471 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  y  e.  A  y )
123 simpr3 1022 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  Fun  ( `' f  |`  A ) )
124 fresf1o 28279 . . . . . . . . . 10  |-  ( ( Fun  f  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) )  ->  ( f  |`  ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> A )
12597, 60, 123, 124syl3anc 1276 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (
f  |`  ( `' f
" A ) ) : ( `' f
" A ) -1-1-onto-> A )
126 simpr 467 . . . . . . . . 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 28249 . . . . . . . 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 5901 . . . . . . . . . 10  |-  ( k  e.  ( `' f
" A )  -> 
( ( f  |`  ( `' f " A
) ) `  k
)  =  ( f `
 k ) )
129128adantl 472 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  k  e.  ( `' f " A ) )  -> 
( ( f  |`  ( `' f " A
) ) `  k
)  =  ( f `
 k ) )
130129disjeq2dv 4391 . . . . . . . 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 263 . . . . . . 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 215 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  k  e.  ( `' f " A ) ( f `
 k ) )
133 disjss3 4414 . . . . . . 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 491 . . . . . 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 1275 . . . . 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 28937 . . . 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 2504 . . 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 4344 . . . . . . 7  |-  U. A  =  U_ x  e.  A  x
13928sselda 3443 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  ~P O )
14040, 139elpwiuncl 28204 . . . . . . 7  |-  ( ph  ->  U_ x  e.  A  x  e.  ~P O
)
141138, 140syl5eqel 2543 . . . . . 6  |-  ( ph  ->  U. A  e.  ~P O )
142141adantr 471 . . . . 5  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  U. A  e.  ~P O )
14319, 142ffvelrnd 6045 . . . 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 1269 . . . . . . . . 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 5887 . . . . . . . . . 10  |-  ( y  =  z  ->  ( M `  y )  =  ( M `  z ) )
147 nfcv 2602 . . . . . . . . . 10  |-  F/_ z
x
148 nfcv 2602 . . . . . . . . . 10  |-  F/_ y
x
149 nfcv 2602 . . . . . . . . . 10  |-  F/_ z
( M `  y
)
150 nfcv 2602 . . . . . . . . . 10  |-  F/_ y
( M `  z
)
151146, 147, 148, 149, 150cbvesum 28911 . . . . . . . . 9  |- Σ* y  e.  x
( M `  y
)  = Σ* z  e.  x
( M `  z
)
152145, 151syl6breq 4455 . . . . . . . 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 5750 . . . . . . . . . 10  |-  ( f : NN --> ( A  u.  { (/) } )  ->  f  Fn  NN )
154 fz1ssnn 11858 . . . . . . . . . . 11  |-  ( 1 ... n )  C_  NN
155 fnssres 5710 . . . . . . . . . . 11  |-  ( ( f  Fn  NN  /\  ( 1 ... n
)  C_  NN )  ->  ( f  |`  (
1 ... n ) )  Fn  ( 1 ... n ) )
156154, 155mpan2 682 . . . . . . . . . 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 12216 . . . . . . . . . 10  |-  ( 1 ... n )  e. 
Fin
159 fnfi 7874 . . . . . . . . . 10  |-  ( ( ( f  |`  (
1 ... n ) )  Fn  ( 1 ... n )  /\  (
1 ... n )  e. 
Fin )  ->  (
f  |`  ( 1 ... n ) )  e. 
Fin )
160158, 159mpan2 682 . . . . . . . . 9  |-  ( ( f  |`  ( 1 ... n ) )  Fn  ( 1 ... n )  ->  (
f  |`  ( 1 ... n ) )  e. 
Fin )
161 rnfi 7882 . . . . . . . . 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 5146 . . . . . . . . . . 11  |-  ( f  |`  ( 1 ... n
) )  C_  f
164 rnss 5081 . . . . . . . . . . 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 3453 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  (toCaraSiga `  M ) )
168166, 37sstrd 3453 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  ( A  u.  {
(/) } ) )
169 nfcv 2602 . . . . . . . . . . . . 13  |-  F/_ z
y
170 nfcv 2602 . . . . . . . . . . . . 13  |-  F/_ y
z
171 id 22 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  y  =  z )
172169, 170, 171cbvdisj 4396 . . . . . . . . . . . 12  |-  (Disj  y  e.  A  y  <-> Disj  z  e.  A  z )
173 disjun0 28253 . . . . . . . . . . . 12  |-  (Disj  z  e.  A  z  -> Disj  z  e.  ( A  u.  { (/)
} ) z )
174172, 173sylbi 200 . . . . . . . . . . 11  |-  (Disj  y  e.  A  y  -> Disj  z  e.  ( A  u.  { (/)
} ) z )
175121, 174syl 17 . . . . . . . . . 10  |-  ( ph  -> Disj  z  e.  ( A  u.  { (/) } ) z )
176175adantr 471 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  z  e.  ( A  u.  { (/)
} ) z )
177 disjss1 4392 . . . . . . . . 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 62 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Disj  z  e. 
ran  ( f  |`  ( 1 ... n
) ) z )
179 pwidg 3975 . . . . . . . . 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 29197 . . . . . . 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 471 . . . . . 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 4235 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  U. ran  ( f  |`  (
1 ... n ) ) 
C_  U. ( A  u.  {
(/) } ) )
184 uniun 4230 . . . . . . . . . . . 12  |-  U. ( A  u.  { (/) } )  =  ( U. A  u.  U. { (/) } )
1852unisn 4226 . . . . . . . . . . . . 13  |-  U. { (/)
}  =  (/)
186185uneq2i 3596 . . . . . . . . . . . 12  |-  ( U. A  u.  U. { (/) } )  =  ( U. A  u.  (/) )
187 un0 3770 . . . . . . . . . . . 12  |-  ( U. A  u.  (/) )  = 
U. A
188184, 186, 1873eqtri 2487 . . . . . . . . . . 11  |-  U. ( A  u.  { (/) } )  =  U. A
189183, 188syl6sseq 3489 . . . . . . . . . 10  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  U. ran  ( f  |`  (
1 ... n ) ) 
C_  U. A )
190189adantr 471 . . . . . . . . 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 4232 . . . . . . . . . . . 12  |-  ( A 
C_  ~P O  ->  U. A  C_ 
U. ~P O )
192 unipw 4663 . . . . . . . . . . . 12  |-  U. ~P O  =  O
193191, 192syl6sseq 3489 . . . . . . . . . . 11  |-  ( A 
C_  ~P O  ->  U. A  C_  O )
19428, 193syl 17 . . . . . . . . . 10  |-  ( ph  ->  U. A  C_  O
)
195194ad2antrr 737 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  U. A  C_  O )
196190, 195sstrd 3453 . . . . . . . 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 3648 . . . . . . . 8  |-  ( U. ran  ( f  |`  (
1 ... n ) ) 
C_  O  <->  ( O  i^i  U. ran  ( f  |`  ( 1 ... n
) ) )  = 
U. ran  ( f  |`  ( 1 ... n
) ) )
198196, 197sylib 201 . . . . . . 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 5891 . . . . . 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 1771 . . . . . . . 8  |-  F/ z ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )
201168adantr 471 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  ( A  u.  {
(/) } ) )
20228ad2antrr 737 . . . . . . . . . . . . . . 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 4129 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  { (/) } 
C_  ~P O )
205202, 204unssd 3621 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ( A  u.  { (/) } ) 
C_  ~P O )
206201, 205sstrd 3453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A )
) )  /\  n  e.  NN )  ->  ran  ( f  |`  (
1 ... n ) ) 
C_  ~P O )
207206sselda 3443 . . . . . . . . . . . 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 3972 . . . . . . . . . . 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 3648 . . . . . . . . . . 11  |-  ( z 
C_  O  <->  ( O  i^i  z )  =  z )
210208, 209sylib 201 . . . . . . . . . 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 5891 . . . . . . . . 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 2813 . . . . . . . 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 28906 . . . . . . 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 5122 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  (
f  |`  ( 1 ... n ) )  =  ( ( k  e.  NN  |->  ( f `  k ) )  |`  ( 1 ... n
) ) )
215214adantr 471 . . . . . . . . . . 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 5172 . . . . . . . . . . . 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 2511 . . . . . . . . . 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 2467 . . . . . . . . 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 5080 . . . . . . . 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 28904 . . . . . . 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 737 . . . . . . . . 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 3443 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f : NN --> ( A  u.  { (/) } )  /\  A  C_  ran  f  /\  Fun  ( `' f  |`  A ) ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  k  e.  NN )
22685adantlr 726 . . . . . . . . . 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 477 . . . . . . . . 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 6045 . . . . . . . 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 467 . . . . . . . . . 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 5891 . . . . . . . . 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 741 . . . . . . . . 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 2495 . . . . . . . 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 4392 . . . . . . . . . . 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 471 . . . . . . . 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 28937 . . . . . . 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 2501 . . . . . 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 2503 . . . . 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 1269 . . . . . . 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 29194 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  ->  ( M `  U. ran  (
f  |`  ( 1 ... n ) ) )  <_  ( M `  U. A ) )
243242adantr 471 . . . . 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 4438 . . . 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 28959 . . 3  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* k  e.  NN ( M `  ( f `
 k ) )  <_  ( M `  U. A ) )
246137, 245eqbrtrrd 4438 . 2  |-  ( (
ph  /\  ( f : NN --> ( A  u.  {
(/) } )  /\  A  C_ 
ran  f  /\  Fun  ( `' f  |`  A ) ) )  -> Σ* z  e.  A
( M `  z
)  <_  ( M `  U. A ) )
2476, 246exlimddv 1791 1  |-  ( ph  -> Σ* z  e.  A ( M `
 z )  <_ 
( M `  U. A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1454   E.wex 1673    e. wcel 1897   A.wral 2748   _Vcvv 3056    \ cdif 3412    u. cun 3413    i^i cin 3414    C_ wss 3415   (/)c0 3742   ~Pcpw 3962   {csn 3979   U.cuni 4211   U_ciun 4291  Disj wdisj 4386   class class class wbr 4415    |-> cmpt 4474   `'ccnv 4851   dom cdm 4852   ran crn 4853    |` cres 4854   "cima 4855   Fun wfun 5594    Fn wfn 5595   -->wf 5596   -1-1-onto->wf1o 5599   ` cfv 5600  (class class class)co 6314   omcom 6718    ~<_ cdom 7592   Fincfn 7594   0cc0 9564   1c1 9565   +oocpnf 9697   RR*cxr 9699    <_ cle 9701   NNcn 10636   [,]cicc 11666   ...cfz 11812  Σ*cesum 28896  toCaraSigaccarsg 29181
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-inf2 8171  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642  ax-addf 9643  ax-mulf 9644
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-iin 4294  df-disj 4387  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-of 6557  df-om 6719  df-1st 6819  df-2nd 6820  df-supp 6941  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-2o 7208  df-oadd 7211  df-er 7388  df-map 7499  df-pm 7500  df-ixp 7548  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-fsupp 7909  df-fi 7950  df-sup 7981  df-inf 7982  df-oi 8050  df-card 8398  df-cda 8623  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-div 10297  df-nn 10637  df-2 10695  df-3 10696  df-4 10697  df-5 10698  df-6 10699  df-7 10700  df-8 10701  df-9 10702  df-10 10703  df-n0 10898  df-z 10966  df-dec 11080  df-uz 11188  df-q 11293  df-rp 11331  df-xneg 11437  df-xadd 11438  df-xmul 11439  df-ioo 11667  df-ioc 11668  df-ico 11669  df-icc 11670  df-fz 11813  df-fzo 11946  df-fl 12059  df-mod 12128  df-seq 12245  df-exp 12304  df-fac 12491  df-bc 12519  df-hash 12547  df-shft 13178  df-cj 13210  df-re 13211  df-im 13212  df-sqrt 13346  df-abs 13347  df-limsup 13574  df-clim 13600  df-rlim 13601  df-sum 13801  df-ef 14169  df-sin 14171  df-cos 14172  df-pi 14174  df-struct 15171  df-ndx 15172  df-slot 15173  df-base 15174  df-sets 15175  df-ress 15176  df-plusg 15251  df-mulr 15252  df-starv 15253  df-sca 15254  df-vsca 15255  df-ip 15256  df-tset 15257  df-ple 15258  df-ds 15260  df-unif 15261  df-hom 15262  df-cco 15263  df-rest 15369  df-topn 15370  df-0g 15388  df-gsum 15389  df-topgen 15390  df-pt 15391  df-prds 15394  df-ordt 15447  df-xrs 15448  df-qtop 15454  df-imas 15455  df-xps 15458  df-mre 15540  df-mrc 15541  df-acs 15543  df-ps 16494  df-tsr 16495  df-plusf 16535  df-mgm 16536  df-sgrp 16575  df-mnd 16585  df-mhm 16630  df-submnd 16631  df-grp 16721  df-minusg 16722  df-sbg 16723  df-mulg 16724  df-subg 16862  df-cntz 17019  df-cmn 17480  df-abl 17481  df-mgp 17772  df-ur 17784  df-ring 17830  df-cring 17831  df-subrg 18054  df-abv 18093  df-lmod 18141  df-scaf 18142  df-sra 18443  df-rgmod 18444  df-psmet 19010  df-xmet 19011  df-met 19012  df-bl 19013  df-mopn 19014  df-fbas 19015  df-fg 19016  df-cnfld 19019  df-top 19969  df-bases 19970  df-topon 19971  df-topsp 19972  df-cld 20082  df-ntr 20083  df-cls 20084  df-nei 20162  df-lp 20200  df-perf 20201  df-cn 20291  df-cnp 20292  df-haus 20379  df-tx 20625  df-hmeo 20818  df-fil 20909  df-fm 21001  df-flim 21002  df-flf 21003  df-tmd 21135  df-tgp 21136  df-tsms 21189  df-trg 21222  df-xms 21383  df-ms 21384  df-tms 21385  df-nm 21645  df-ngp 21646  df-nrg 21648  df-nlm 21649  df-ii 21957  df-cncf 21958  df-limc 22869  df-dv 22870  df-log 23554  df-esum 28897  df-carsg 29182
This theorem is referenced by:  omsmeas  29203  omsmeasOLD  29204
  Copyright terms: Public domain W3C validator