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

Theorem volfiniune 28072
Description: The Lebesgue measure function is countably additive. This theorem is to volfiniun 21827 what voliune 28071 is to voliun 21834. (Contributed by Thierry Arnoux, 16-Oct-2017.)
Assertion
Ref Expression
volfiniune  |-  ( ( A  e.  Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  -> 
( vol `  U_ n  e.  A  B )  = Σ* n  e.  A ( vol `  B ) )
Distinct variable group:    A, n
Allowed substitution hint:    B( n)

Proof of Theorem volfiniune
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 simpl1 998 . . . 4  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B
)  e.  RR )  ->  A  e.  Fin )
2 simpl2 999 . . . . 5  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B
)  e.  RR )  ->  A. n  e.  A  B  e.  dom  vol )
3 simpr 461 . . . . 5  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B
)  e.  RR )  ->  A. n  e.  A  ( vol `  B )  e.  RR )
4 r19.26 2968 . . . . 5  |-  ( A. n  e.  A  ( B  e.  dom  vol  /\  ( vol `  B )  e.  RR )  <->  ( A. n  e.  A  B  e.  dom  vol  /\  A. n  e.  A  ( vol `  B )  e.  RR ) )
52, 3, 4sylanbrc 664 . . . 4  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B
)  e.  RR )  ->  A. n  e.  A  ( B  e.  dom  vol 
/\  ( vol `  B
)  e.  RR ) )
6 simpl3 1000 . . . 4  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B
)  e.  RR )  -> Disj  n  e.  A  B
)
7 volfiniun 21827 . . . 4  |-  ( ( A  e.  Fin  /\  A. n  e.  A  ( B  e.  dom  vol  /\  ( vol `  B
)  e.  RR )  /\ Disj  n  e.  A  B
)  ->  ( vol ` 
U_ n  e.  A  B )  =  sum_ n  e.  A  ( vol `  B ) )
81, 5, 6, 7syl3anc 1227 . . 3  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B
)  e.  RR )  ->  ( vol `  U_ n  e.  A  B )  =  sum_ n  e.  A  ( vol `  B ) )
9 nfcv 2603 . . . 4  |-  F/_ n A
109nfel1 2619 . . . . . 6  |-  F/ n  A  e.  Fin
11 nfra1 2822 . . . . . 6  |-  F/ n A. n  e.  A  B  e.  dom  vol
12 nfdisj1 4417 . . . . . 6  |-  F/ nDisj  n  e.  A  B
1310, 11, 12nf3an 1914 . . . . 5  |-  F/ n
( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )
14 nfra1 2822 . . . . 5  |-  F/ n A. n  e.  A  ( vol `  B )  e.  RR
1513, 14nfan 1912 . . . 4  |-  F/ n
( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B )  e.  RR )
163r19.21bi 2810 . . . . 5  |-  ( ( ( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B )  e.  RR )  /\  n  e.  A )  ->  ( vol `  B )  e.  RR )
17 rspa 2808 . . . . . . . 8  |-  ( ( A. n  e.  A  B  e.  dom  vol  /\  n  e.  A )  ->  B  e.  dom  vol )
18 volf 21810 . . . . . . . . 9  |-  vol : dom  vol --> ( 0 [,] +oo )
1918ffvelrni 6012 . . . . . . . 8  |-  ( B  e.  dom  vol  ->  ( vol `  B )  e.  ( 0 [,] +oo ) )
2017, 19syl 16 . . . . . . 7  |-  ( ( A. n  e.  A  B  e.  dom  vol  /\  n  e.  A )  ->  ( vol `  B
)  e.  ( 0 [,] +oo ) )
212, 20sylan 471 . . . . . 6  |-  ( ( ( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B )  e.  RR )  /\  n  e.  A )  ->  ( vol `  B )  e.  ( 0 [,] +oo ) )
22 0xr 9640 . . . . . . . 8  |-  0  e.  RR*
23 pnfxr 11327 . . . . . . . 8  |- +oo  e.  RR*
24 elicc1 11579 . . . . . . . 8  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR* )  ->  (
( vol `  B
)  e.  ( 0 [,] +oo )  <->  ( ( vol `  B )  e. 
RR*  /\  0  <_  ( vol `  B )  /\  ( vol `  B
)  <_ +oo )
) )
2522, 23, 24mp2an 672 . . . . . . 7  |-  ( ( vol `  B )  e.  ( 0 [,] +oo )  <->  ( ( vol `  B )  e.  RR*  /\  0  <_  ( vol `  B )  /\  ( vol `  B )  <_ +oo ) )
2625simp2bi 1011 . . . . . 6  |-  ( ( vol `  B )  e.  ( 0 [,] +oo )  ->  0  <_ 
( vol `  B
) )
2721, 26syl 16 . . . . 5  |-  ( ( ( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B )  e.  RR )  /\  n  e.  A )  ->  0  <_  ( vol `  B
) )
28 ltpnf 11337 . . . . . 6  |-  ( ( vol `  B )  e.  RR  ->  ( vol `  B )  < +oo )
2916, 28syl 16 . . . . 5  |-  ( ( ( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B )  e.  RR )  /\  n  e.  A )  ->  ( vol `  B )  < +oo )
30 0re 9596 . . . . . 6  |-  0  e.  RR
31 elico2 11594 . . . . . 6  |-  ( ( 0  e.  RR  /\ +oo  e.  RR* )  ->  (
( vol `  B
)  e.  ( 0 [,) +oo )  <->  ( ( vol `  B )  e.  RR  /\  0  <_ 
( vol `  B
)  /\  ( vol `  B )  < +oo ) ) )
3230, 23, 31mp2an 672 . . . . 5  |-  ( ( vol `  B )  e.  ( 0 [,) +oo )  <->  ( ( vol `  B )  e.  RR  /\  0  <_  ( vol `  B )  /\  ( vol `  B )  < +oo ) )
3316, 27, 29, 32syl3anbrc 1179 . . . 4  |-  ( ( ( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B )  e.  RR )  /\  n  e.  A )  ->  ( vol `  B )  e.  ( 0 [,) +oo ) )
349, 15, 1, 33esumpfinvalf 27952 . . 3  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B
)  e.  RR )  -> Σ* n  e.  A ( vol `  B )  =  sum_ n  e.  A  ( vol `  B ) )
358, 34eqtr4d 2485 . 2  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  A. n  e.  A  ( vol `  B
)  e.  RR )  ->  ( vol `  U_ n  e.  A  B )  = Σ* n  e.  A ( vol `  B ) )
36 simpr 461 . . . . . . . 8  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  E. n  e.  A  ( vol `  B )  = +oo )
37 nfv 1692 . . . . . . . . 9  |-  F/ k ( vol `  B
)  = +oo
38 nfcv 2603 . . . . . . . . . . 11  |-  F/_ n vol
39 nfcsb1v 3434 . . . . . . . . . . 11  |-  F/_ n [_ k  /  n ]_ B
4038, 39nffv 5860 . . . . . . . . . 10  |-  F/_ n
( vol `  [_ k  /  n ]_ B )
4140nfeq1 2618 . . . . . . . . 9  |-  F/ n
( vol `  [_ k  /  n ]_ B )  = +oo
42 csbeq1a 3427 . . . . . . . . . . 11  |-  ( n  =  k  ->  B  =  [_ k  /  n ]_ B )
4342fveq2d 5857 . . . . . . . . . 10  |-  ( n  =  k  ->  ( vol `  B )  =  ( vol `  [_ k  /  n ]_ B ) )
4443eqeq1d 2443 . . . . . . . . 9  |-  ( n  =  k  ->  (
( vol `  B
)  = +oo  <->  ( vol ` 
[_ k  /  n ]_ B )  = +oo ) )
4537, 41, 44cbvrex 3065 . . . . . . . 8  |-  ( E. n  e.  A  ( vol `  B )  = +oo  <->  E. k  e.  A  ( vol ` 
[_ k  /  n ]_ B )  = +oo )
4636, 45sylib 196 . . . . . . 7  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  E. k  e.  A  ( vol `  [_ k  /  n ]_ B )  = +oo )
4739nfel1 2619 . . . . . . . . . . . . . 14  |-  F/ n [_ k  /  n ]_ B  e.  dom  vol
4842eleq1d 2510 . . . . . . . . . . . . . 14  |-  ( n  =  k  ->  ( B  e.  dom  vol  <->  [_ k  /  n ]_ B  e.  dom  vol ) )
4947, 48rspc 3188 . . . . . . . . . . . . 13  |-  ( k  e.  A  ->  ( A. n  e.  A  B  e.  dom  vol  ->  [_ k  /  n ]_ B  e.  dom  vol )
)
5049impcom 430 . . . . . . . . . . . 12  |-  ( ( A. n  e.  A  B  e.  dom  vol  /\  k  e.  A )  ->  [_ k  /  n ]_ B  e.  dom  vol )
5150adantll 713 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol )  /\  k  e.  A
)  ->  [_ k  /  n ]_ B  e.  dom  vol )
52 finiunmbl 21824 . . . . . . . . . . . 12  |-  ( ( A  e.  Fin  /\  A. n  e.  A  B  e.  dom  vol )  ->  U_ n  e.  A  B  e.  dom  vol )
5352adantr 465 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol )  /\  k  e.  A
)  ->  U_ n  e.  A  B  e.  dom  vol )
54 nfcv 2603 . . . . . . . . . . . . 13  |-  F/_ n
k
559, 54, 39, 42ssiun2sf 27296 . . . . . . . . . . . 12  |-  ( k  e.  A  ->  [_ k  /  n ]_ B  C_  U_ n  e.  A  B
)
5655adantl 466 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol )  /\  k  e.  A
)  ->  [_ k  /  n ]_ B  C_  U_ n  e.  A  B )
57 volss 21814 . . . . . . . . . . 11  |-  ( (
[_ k  /  n ]_ B  e.  dom  vol 
/\  U_ n  e.  A  B  e.  dom  vol  /\  [_ k  /  n ]_ B  C_  U_ n  e.  A  B )  -> 
( vol `  [_ k  /  n ]_ B )  <_  ( vol `  U_ n  e.  A  B )
)
5851, 53, 56, 57syl3anc 1227 . . . . . . . . . 10  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol )  /\  k  e.  A
)  ->  ( vol ` 
[_ k  /  n ]_ B )  <_  ( vol `  U_ n  e.  A  B ) )
59583adantl3 1153 . . . . . . . . 9  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  k  e.  A
)  ->  ( vol ` 
[_ k  /  n ]_ B )  <_  ( vol `  U_ n  e.  A  B ) )
6059adantlr 714 . . . . . . . 8  |-  ( ( ( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B )  = +oo )  /\  k  e.  A )  ->  ( vol `  [_ k  /  n ]_ B )  <_ 
( vol `  U_ n  e.  A  B )
)
6160ralrimiva 2855 . . . . . . 7  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  A. k  e.  A  ( vol `  [_ k  /  n ]_ B )  <_  ( vol `  U_ n  e.  A  B )
)
62 r19.29r 2977 . . . . . . 7  |-  ( ( E. k  e.  A  ( vol `  [_ k  /  n ]_ B )  = +oo  /\  A. k  e.  A  ( vol `  [_ k  /  n ]_ B )  <_ 
( vol `  U_ n  e.  A  B )
)  ->  E. k  e.  A  ( ( vol `  [_ k  /  n ]_ B )  = +oo  /\  ( vol `  [_ k  /  n ]_ B )  <_  ( vol `  U_ n  e.  A  B ) ) )
6346, 61, 62syl2anc 661 . . . . . 6  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  E. k  e.  A  ( ( vol `  [_ k  /  n ]_ B )  = +oo  /\  ( vol `  [_ k  /  n ]_ B )  <_ 
( vol `  U_ n  e.  A  B )
) )
64 breq1 4437 . . . . . . . 8  |-  ( ( vol `  [_ k  /  n ]_ B )  = +oo  ->  (
( vol `  [_ k  /  n ]_ B )  <_  ( vol `  U_ n  e.  A  B )  <-> +oo 
<_  ( vol `  U_ n  e.  A  B )
) )
6564biimpa 484 . . . . . . 7  |-  ( ( ( vol `  [_ k  /  n ]_ B )  = +oo  /\  ( vol `  [_ k  /  n ]_ B )  <_ 
( vol `  U_ n  e.  A  B )
)  -> +oo  <_  ( vol `  U_ n  e.  A  B ) )
6665reximi 2909 . . . . . 6  |-  ( E. k  e.  A  ( ( vol `  [_ k  /  n ]_ B )  = +oo  /\  ( vol `  [_ k  /  n ]_ B )  <_ 
( vol `  U_ n  e.  A  B )
)  ->  E. k  e.  A +oo  <_  ( vol `  U_ n  e.  A  B ) )
6763, 66syl 16 . . . . 5  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  E. k  e.  A +oo  <_  ( vol `  U_ n  e.  A  B )
)
68 rexex 2898 . . . . . 6  |-  ( E. k  e.  A +oo  <_  ( vol `  U_ n  e.  A  B )  ->  E. k +oo  <_  ( vol `  U_ n  e.  A  B )
)
69 19.9v 1739 . . . . . 6  |-  ( E. k +oo  <_  ( vol `  U_ n  e.  A  B )  <-> +oo  <_  ( vol `  U_ n  e.  A  B ) )
7068, 69sylib 196 . . . . 5  |-  ( E. k  e.  A +oo  <_  ( vol `  U_ n  e.  A  B )  -> +oo  <_  ( vol ` 
U_ n  e.  A  B ) )
7167, 70syl 16 . . . 4  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  -> +oo  <_  ( vol ` 
U_ n  e.  A  B ) )
72 iccssxr 11613 . . . . . . . . 9  |-  ( 0 [,] +oo )  C_  RR*
7318ffvelrni 6012 . . . . . . . . 9  |-  ( U_ n  e.  A  B  e.  dom  vol  ->  ( vol `  U_ n  e.  A  B )  e.  ( 0 [,] +oo )
)
7472, 73sseldi 3485 . . . . . . . 8  |-  ( U_ n  e.  A  B  e.  dom  vol  ->  ( vol `  U_ n  e.  A  B )  e.  RR* )
7552, 74syl 16 . . . . . . 7  |-  ( ( A  e.  Fin  /\  A. n  e.  A  B  e.  dom  vol )  -> 
( vol `  U_ n  e.  A  B )  e.  RR* )
76753adant3 1015 . . . . . 6  |-  ( ( A  e.  Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  -> 
( vol `  U_ n  e.  A  B )  e.  RR* )
7776adantr 465 . . . . 5  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  ( vol `  U_ n  e.  A  B )  e.  RR* )
78 xgepnf 27439 . . . . 5  |-  ( ( vol `  U_ n  e.  A  B )  e.  RR*  ->  ( +oo  <_  ( vol `  U_ n  e.  A  B )  <->  ( vol `  U_ n  e.  A  B )  = +oo ) )
7977, 78syl 16 . . . 4  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  ( +oo  <_  ( vol `  U_ n  e.  A  B )  <->  ( vol ` 
U_ n  e.  A  B )  = +oo ) )
8071, 79mpbid 210 . . 3  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  ( vol `  U_ n  e.  A  B )  = +oo )
81 nfre1 2902 . . . . 5  |-  F/ n E. n  e.  A  ( vol `  B )  = +oo
8213, 81nfan 1912 . . . 4  |-  F/ n
( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B )  = +oo )
83 simpl1 998 . . . 4  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  A  e.  Fin )
84203ad2antl2 1158 . . . . 5  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  n  e.  A
)  ->  ( vol `  B )  e.  ( 0 [,] +oo )
)
8584adantlr 714 . . . 4  |-  ( ( ( ( A  e. 
Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B )  = +oo )  /\  n  e.  A )  ->  ( vol `  B )  e.  ( 0 [,] +oo ) )
8682, 83, 85, 36esumpinfval 27949 . . 3  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  -> Σ* n  e.  A ( vol `  B )  = +oo )
8780, 86eqtr4d 2485 . 2  |-  ( ( ( A  e.  Fin  /\ 
A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  /\  E. n  e.  A  ( vol `  B
)  = +oo )  ->  ( vol `  U_ n  e.  A  B )  = Σ* n  e.  A ( vol `  B ) )
88 exmid 415 . . . . 5  |-  ( A. n  e.  A  ( vol `  B )  e.  RR  \/  -.  A. n  e.  A  ( vol `  B )  e.  RR )
89 rexnal 2889 . . . . . 6  |-  ( E. n  e.  A  -.  ( vol `  B )  e.  RR  <->  -.  A. n  e.  A  ( vol `  B )  e.  RR )
9089orbi2i 519 . . . . 5  |-  ( ( A. n  e.  A  ( vol `  B )  e.  RR  \/  E. n  e.  A  -.  ( vol `  B )  e.  RR )  <->  ( A. n  e.  A  ( vol `  B )  e.  RR  \/  -.  A. n  e.  A  ( vol `  B )  e.  RR ) )
9188, 90mpbir 209 . . . 4  |-  ( A. n  e.  A  ( vol `  B )  e.  RR  \/  E. n  e.  A  -.  ( vol `  B )  e.  RR )
92 r19.29 2976 . . . . . . 7  |-  ( ( A. n  e.  A  B  e.  dom  vol  /\  E. n  e.  A  -.  ( vol `  B )  e.  RR )  ->  E. n  e.  A  ( B  e.  dom  vol 
/\  -.  ( vol `  B )  e.  RR ) )
93 xrge0nre 27550 . . . . . . . . 9  |-  ( ( ( vol `  B
)  e.  ( 0 [,] +oo )  /\  -.  ( vol `  B
)  e.  RR )  ->  ( vol `  B
)  = +oo )
9419, 93sylan 471 . . . . . . . 8  |-  ( ( B  e.  dom  vol  /\ 
-.  ( vol `  B
)  e.  RR )  ->  ( vol `  B
)  = +oo )
9594reximi 2909 . . . . . . 7  |-  ( E. n  e.  A  ( B  e.  dom  vol  /\ 
-.  ( vol `  B
)  e.  RR )  ->  E. n  e.  A  ( vol `  B )  = +oo )
9692, 95syl 16 . . . . . 6  |-  ( ( A. n  e.  A  B  e.  dom  vol  /\  E. n  e.  A  -.  ( vol `  B )  e.  RR )  ->  E. n  e.  A  ( vol `  B )  = +oo )
9796ex 434 . . . . 5  |-  ( A. n  e.  A  B  e.  dom  vol  ->  ( E. n  e.  A  -.  ( vol `  B )  e.  RR  ->  E. n  e.  A  ( vol `  B )  = +oo ) )
9897orim2d 838 . . . 4  |-  ( A. n  e.  A  B  e.  dom  vol  ->  ( ( A. n  e.  A  ( vol `  B )  e.  RR  \/  E. n  e.  A  -.  ( vol `  B )  e.  RR )  -> 
( A. n  e.  A  ( vol `  B
)  e.  RR  \/  E. n  e.  A  ( vol `  B )  = +oo ) ) )
9991, 98mpi 17 . . 3  |-  ( A. n  e.  A  B  e.  dom  vol  ->  ( A. n  e.  A  ( vol `  B )  e.  RR  \/  E. n  e.  A  ( vol `  B )  = +oo ) )
100993ad2ant2 1017 . 2  |-  ( ( A  e.  Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  -> 
( A. n  e.  A  ( vol `  B
)  e.  RR  \/  E. n  e.  A  ( vol `  B )  = +oo ) )
10135, 87, 100mpjaodan 784 1  |-  ( ( A  e.  Fin  /\  A. n  e.  A  B  e.  dom  vol  /\ Disj  n  e.  A  B )  -> 
( vol `  U_ n  e.  A  B )  = Σ* n  e.  A ( vol `  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 972    = wceq 1381   E.wex 1597    e. wcel 1802   A.wral 2791   E.wrex 2792   [_csb 3418    C_ wss 3459   U_ciun 4312  Disj wdisj 4404   class class class wbr 4434   dom cdm 4986   ` cfv 5575  (class class class)co 6278   Fincfn 7515   RRcr 9491   0cc0 9492   +oocpnf 9625   RR*cxr 9627    < clt 9628    <_ cle 9629   [,)cico 11537   [,]cicc 11538   sum_csu 13484   volcvol 21745  Σ*cesum 27910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4545  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574  ax-inf2 8058  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570  ax-addf 9571  ax-mulf 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-pss 3475  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-tp 4016  df-op 4018  df-uni 4232  df-int 4269  df-iun 4314  df-iin 4315  df-disj 4405  df-br 4435  df-opab 4493  df-mpt 4494  df-tr 4528  df-eprel 4778  df-id 4782  df-po 4787  df-so 4788  df-fr 4825  df-se 4826  df-we 4827  df-ord 4868  df-on 4869  df-lim 4870  df-suc 4871  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-isom 5584  df-riota 6239  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-of 6522  df-om 6683  df-1st 6782  df-2nd 6783  df-supp 6901  df-recs 7041  df-rdg 7075  df-1o 7129  df-2o 7130  df-oadd 7133  df-er 7310  df-map 7421  df-pm 7422  df-ixp 7469  df-en 7516  df-dom 7517  df-sdom 7518  df-fin 7519  df-fsupp 7829  df-fi 7870  df-sup 7900  df-oi 7935  df-card 8320  df-cda 8548  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9809  df-neg 9810  df-div 10210  df-nn 10540  df-2 10597  df-3 10598  df-4 10599  df-5 10600  df-6 10601  df-7 10602  df-8 10603  df-9 10604  df-10 10605  df-n0 10799  df-z 10868  df-dec 10982  df-uz 11088  df-q 11189  df-rp 11227  df-xneg 11324  df-xadd 11325  df-xmul 11326  df-ioo 11539  df-ioc 11540  df-ico 11541  df-icc 11542  df-fz 11679  df-fzo 11801  df-fl 11905  df-mod 11973  df-seq 12084  df-exp 12143  df-fac 12330  df-bc 12357  df-hash 12382  df-shft 12876  df-cj 12908  df-re 12909  df-im 12910  df-sqrt 13044  df-abs 13045  df-limsup 13270  df-clim 13287  df-rlim 13288  df-sum 13485  df-ef 13678  df-sin 13680  df-cos 13681  df-pi 13683  df-struct 14508  df-ndx 14509  df-slot 14510  df-base 14511  df-sets 14512  df-ress 14513  df-plusg 14584  df-mulr 14585  df-starv 14586  df-sca 14587  df-vsca 14588  df-ip 14589  df-tset 14590  df-ple 14591  df-ds 14593  df-unif 14594  df-hom 14595  df-cco 14596  df-rest 14694  df-topn 14695  df-0g 14713  df-gsum 14714  df-topgen 14715  df-pt 14716  df-prds 14719  df-ordt 14772  df-xrs 14773  df-qtop 14778  df-imas 14779  df-xps 14781  df-mre 14857  df-mrc 14858  df-acs 14860  df-ps 15701  df-tsr 15702  df-plusf 15742  df-mgm 15743  df-sgrp 15782  df-mnd 15792  df-mhm 15837  df-submnd 15838  df-grp 15928  df-minusg 15929  df-sbg 15930  df-mulg 15931  df-subg 16069  df-cntz 16226  df-cmn 16671  df-abl 16672  df-mgp 17013  df-ur 17025  df-ring 17071  df-cring 17072  df-subrg 17298  df-abv 17337  df-lmod 17385  df-scaf 17386  df-sra 17689  df-rgmod 17690  df-psmet 18282  df-xmet 18283  df-met 18284  df-bl 18285  df-mopn 18286  df-fbas 18287  df-fg 18288  df-cnfld 18292  df-top 19269  df-bases 19271  df-topon 19272  df-topsp 19273  df-cld 19390  df-ntr 19391  df-cls 19392  df-nei 19469  df-lp 19507  df-perf 19508  df-cn 19598  df-cnp 19599  df-haus 19686  df-tx 19933  df-hmeo 20126  df-fil 20217  df-fm 20309  df-flim 20310  df-flf 20311  df-tmd 20441  df-tgp 20442  df-tsms 20495  df-trg 20532  df-xms 20693  df-ms 20694  df-tms 20695  df-nm 20973  df-ngp 20974  df-nrg 20976  df-nlm 20977  df-ii 21251  df-cncf 21252  df-ovol 21746  df-vol 21747  df-limc 22140  df-dv 22141  df-log 22813  df-esum 27911
This theorem is referenced by:  volmeas  28073
  Copyright terms: Public domain W3C validator