This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem volfiniun

Description: The volume of a disjoint finite union of measurable sets is the sum of the measures. (Contributed by Mario Carneiro, 25-Jun-2014) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion volfiniun 
|- ( ( A e. Fin /\ A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. A B ) -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) )

Proof

Step Hyp Ref Expression
1 raleq 
 |-  ( w = (/) -> ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) <-> A. k e. (/) ( B e. dom vol /\ ( vol ` B ) e. RR ) ) )
2 disjeq1 
 |-  ( w = (/) -> ( Disj_ k e. w B <-> Disj_ k e. (/) B ) )
3 1 2 anbi12d 
 |-  ( w = (/) -> ( ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. w B ) <-> ( A. k e. (/) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. (/) B ) ) )
4 iuneq1 
 |-  ( w = (/) -> U_ k e. w B = U_ k e. (/) B )
5 4 fveq2d 
 |-  ( w = (/) -> ( vol ` U_ k e. w B ) = ( vol ` U_ k e. (/) B ) )
6 sumeq1 
 |-  ( w = (/) -> sum_ k e. w ( vol ` B ) = sum_ k e. (/) ( vol ` B ) )
7 5 6 eqeq12d 
 |-  ( w = (/) -> ( ( vol ` U_ k e. w B ) = sum_ k e. w ( vol ` B ) <-> ( vol ` U_ k e. (/) B ) = sum_ k e. (/) ( vol ` B ) ) )
8 3 7 imbi12d 
 |-  ( w = (/) -> ( ( ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. w B ) -> ( vol ` U_ k e. w B ) = sum_ k e. w ( vol ` B ) ) <-> ( ( A. k e. (/) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. (/) B ) -> ( vol ` U_ k e. (/) B ) = sum_ k e. (/) ( vol ` B ) ) ) )
9 raleq 
 |-  ( w = y -> ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) <-> A. k e. y ( B e. dom vol /\ ( vol ` B ) e. RR ) ) )
10 disjeq1 
 |-  ( w = y -> ( Disj_ k e. w B <-> Disj_ k e. y B ) )
11 9 10 anbi12d 
 |-  ( w = y -> ( ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. w B ) <-> ( A. k e. y ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. y B ) ) )
12 iuneq1 
 |-  ( w = y -> U_ k e. w B = U_ k e. y B )
13 12 fveq2d 
 |-  ( w = y -> ( vol ` U_ k e. w B ) = ( vol ` U_ k e. y B ) )
14 sumeq1 
 |-  ( w = y -> sum_ k e. w ( vol ` B ) = sum_ k e. y ( vol ` B ) )
15 13 14 eqeq12d 
 |-  ( w = y -> ( ( vol ` U_ k e. w B ) = sum_ k e. w ( vol ` B ) <-> ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) ) )
16 11 15 imbi12d 
 |-  ( w = y -> ( ( ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. w B ) -> ( vol ` U_ k e. w B ) = sum_ k e. w ( vol ` B ) ) <-> ( ( A. k e. y ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. y B ) -> ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) ) ) )
17 raleq 
 |-  ( w = ( y u. { z } ) -> ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) <-> A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) ) )
18 disjeq1 
 |-  ( w = ( y u. { z } ) -> ( Disj_ k e. w B <-> Disj_ k e. ( y u. { z } ) B ) )
19 17 18 anbi12d 
 |-  ( w = ( y u. { z } ) -> ( ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. w B ) <-> ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) )
20 iuneq1 
 |-  ( w = ( y u. { z } ) -> U_ k e. w B = U_ k e. ( y u. { z } ) B )
21 20 fveq2d 
 |-  ( w = ( y u. { z } ) -> ( vol ` U_ k e. w B ) = ( vol ` U_ k e. ( y u. { z } ) B ) )
22 sumeq1 
 |-  ( w = ( y u. { z } ) -> sum_ k e. w ( vol ` B ) = sum_ k e. ( y u. { z } ) ( vol ` B ) )
23 21 22 eqeq12d 
 |-  ( w = ( y u. { z } ) -> ( ( vol ` U_ k e. w B ) = sum_ k e. w ( vol ` B ) <-> ( vol ` U_ k e. ( y u. { z } ) B ) = sum_ k e. ( y u. { z } ) ( vol ` B ) ) )
24 19 23 imbi12d 
 |-  ( w = ( y u. { z } ) -> ( ( ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. w B ) -> ( vol ` U_ k e. w B ) = sum_ k e. w ( vol ` B ) ) <-> ( ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) -> ( vol ` U_ k e. ( y u. { z } ) B ) = sum_ k e. ( y u. { z } ) ( vol ` B ) ) ) )
25 raleq 
 |-  ( w = A -> ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) <-> A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) ) )
26 disjeq1 
 |-  ( w = A -> ( Disj_ k e. w B <-> Disj_ k e. A B ) )
27 25 26 anbi12d 
 |-  ( w = A -> ( ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. w B ) <-> ( A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. A B ) ) )
28 iuneq1 
 |-  ( w = A -> U_ k e. w B = U_ k e. A B )
29 28 fveq2d 
 |-  ( w = A -> ( vol ` U_ k e. w B ) = ( vol ` U_ k e. A B ) )
30 sumeq1 
 |-  ( w = A -> sum_ k e. w ( vol ` B ) = sum_ k e. A ( vol ` B ) )
31 29 30 eqeq12d 
 |-  ( w = A -> ( ( vol ` U_ k e. w B ) = sum_ k e. w ( vol ` B ) <-> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) ) )
32 27 31 imbi12d 
 |-  ( w = A -> ( ( ( A. k e. w ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. w B ) -> ( vol ` U_ k e. w B ) = sum_ k e. w ( vol ` B ) ) <-> ( ( A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. A B ) -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) ) ) )
33 0mbl 
 |-  (/) e. dom vol
34 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
35 33 34 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
36 ovol0 
 |-  ( vol* ` (/) ) = 0
37 35 36 eqtri 
 |-  ( vol ` (/) ) = 0
38 0iun 
 |-  U_ k e. (/) B = (/)
39 38 fveq2i 
 |-  ( vol ` U_ k e. (/) B ) = ( vol ` (/) )
40 sum0 
 |-  sum_ k e. (/) ( vol ` B ) = 0
41 37 39 40 3eqtr4i 
 |-  ( vol ` U_ k e. (/) B ) = sum_ k e. (/) ( vol ` B )
42 41 a1i 
 |-  ( ( A. k e. (/) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. (/) B ) -> ( vol ` U_ k e. (/) B ) = sum_ k e. (/) ( vol ` B ) )
43 ssun1 
 |-  y C_ ( y u. { z } )
44 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) -> A. k e. y ( B e. dom vol /\ ( vol ` B ) e. RR ) ) )
45 43 44 ax-mp 
 |-  ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) -> A. k e. y ( B e. dom vol /\ ( vol ` B ) e. RR ) )
46 disjss1 
 |-  ( y C_ ( y u. { z } ) -> ( Disj_ k e. ( y u. { z } ) B -> Disj_ k e. y B ) )
47 43 46 ax-mp 
 |-  ( Disj_ k e. ( y u. { z } ) B -> Disj_ k e. y B )
48 45 47 anim12i 
 |-  ( ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) -> ( A. k e. y ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. y B ) )
49 48 imim1i 
 |-  ( ( ( A. k e. y ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. y B ) -> ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) ) -> ( ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) -> ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) ) )
50 oveq1 
 |-  ( ( vol ` U_ m e. y [_ m / k ]_ B ) = sum_ m e. y ( vol ` [_ m / k ]_ B ) -> ( ( vol ` U_ m e. y [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) = ( sum_ m e. y ( vol ` [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) )
51 iunxun 
 |-  U_ m e. ( y u. { z } ) [_ m / k ]_ B = ( U_ m e. y [_ m / k ]_ B u. U_ m e. { z } [_ m / k ]_ B )
52 vex 
 |-  z e. _V
53 csbeq1 
 |-  ( m = z -> [_ m / k ]_ B = [_ z / k ]_ B )
54 52 53 iunxsn 
 |-  U_ m e. { z } [_ m / k ]_ B = [_ z / k ]_ B
55 54 uneq2i 
 |-  ( U_ m e. y [_ m / k ]_ B u. U_ m e. { z } [_ m / k ]_ B ) = ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B )
56 51 55 eqtri 
 |-  U_ m e. ( y u. { z } ) [_ m / k ]_ B = ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B )
57 56 fveq2i 
 |-  ( vol ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) = ( vol ` ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B ) )
58 nfcv 
 |-  F/_ m B
59 nfcsb1v 
 |-  F/_ k [_ m / k ]_ B
60 csbeq1a 
 |-  ( k = m -> B = [_ m / k ]_ B )
61 58 59 60 cbviun 
 |-  U_ k e. y B = U_ m e. y [_ m / k ]_ B
62 simpll 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> y e. Fin )
63 simprl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) )
64 simpl 
 |-  ( ( B e. dom vol /\ ( vol ` B ) e. RR ) -> B e. dom vol )
65 64 ralimi 
 |-  ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) -> A. k e. ( y u. { z } ) B e. dom vol )
66 63 65 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> A. k e. ( y u. { z } ) B e. dom vol )
67 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. k e. ( y u. { z } ) B e. dom vol -> A. k e. y B e. dom vol ) )
68 43 66 67 mpsyl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> A. k e. y B e. dom vol )
69 finiunmbl 
 |-  ( ( y e. Fin /\ A. k e. y B e. dom vol ) -> U_ k e. y B e. dom vol )
70 62 68 69 syl2anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> U_ k e. y B e. dom vol )
71 61 70 eqeltrrid 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> U_ m e. y [_ m / k ]_ B e. dom vol )
72 ssun2 
 |-  { z } C_ ( y u. { z } )
73 vsnid 
 |-  z e. { z }
74 72 73 sselii 
 |-  z e. ( y u. { z } )
75 nfcsb1v 
 |-  F/_ k [_ z / k ]_ B
76 75 nfel1 
 |-  F/ k [_ z / k ]_ B e. dom vol
77 nfcv 
 |-  F/_ k vol
78 77 75 nffv 
 |-  F/_ k ( vol ` [_ z / k ]_ B )
79 78 nfel1 
 |-  F/ k ( vol ` [_ z / k ]_ B ) e. RR
80 76 79 nfan 
 |-  F/ k ( [_ z / k ]_ B e. dom vol /\ ( vol ` [_ z / k ]_ B ) e. RR )
81 csbeq1a 
 |-  ( k = z -> B = [_ z / k ]_ B )
82 81 eleq1d 
 |-  ( k = z -> ( B e. dom vol <-> [_ z / k ]_ B e. dom vol ) )
83 81 fveq2d 
 |-  ( k = z -> ( vol ` B ) = ( vol ` [_ z / k ]_ B ) )
84 83 eleq1d 
 |-  ( k = z -> ( ( vol ` B ) e. RR <-> ( vol ` [_ z / k ]_ B ) e. RR ) )
85 82 84 anbi12d 
 |-  ( k = z -> ( ( B e. dom vol /\ ( vol ` B ) e. RR ) <-> ( [_ z / k ]_ B e. dom vol /\ ( vol ` [_ z / k ]_ B ) e. RR ) ) )
86 80 85 rspc 
 |-  ( z e. ( y u. { z } ) -> ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) -> ( [_ z / k ]_ B e. dom vol /\ ( vol ` [_ z / k ]_ B ) e. RR ) ) )
87 74 63 86 mpsyl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( [_ z / k ]_ B e. dom vol /\ ( vol ` [_ z / k ]_ B ) e. RR ) )
88 87 simpld 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> [_ z / k ]_ B e. dom vol )
89 simplr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> -. z e. y )
90 elin 
 |-  ( w e. ( U_ m e. y [_ m / k ]_ B i^i [_ z / k ]_ B ) <-> ( w e. U_ m e. y [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) )
91 eliun 
 |-  ( w e. U_ m e. y [_ m / k ]_ B <-> E. m e. y w e. [_ m / k ]_ B )
92 simplrr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> Disj_ k e. ( y u. { z } ) B )
93 nfcv 
 |-  F/_ n B
94 nfcsb1v 
 |-  F/_ k [_ n / k ]_ B
95 csbeq1a 
 |-  ( k = n -> B = [_ n / k ]_ B )
96 93 94 95 cbvdisj 
 |-  ( Disj_ k e. ( y u. { z } ) B <-> Disj_ n e. ( y u. { z } ) [_ n / k ]_ B )
97 92 96 sylib 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> Disj_ n e. ( y u. { z } ) [_ n / k ]_ B )
98 simpr1 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> m e. y )
99 elun1 
 |-  ( m e. y -> m e. ( y u. { z } ) )
100 98 99 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> m e. ( y u. { z } ) )
101 74 a1i 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> z e. ( y u. { z } ) )
102 simpr2 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> w e. [_ m / k ]_ B )
103 simpr3 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> w e. [_ z / k ]_ B )
104 csbeq1 
 |-  ( n = m -> [_ n / k ]_ B = [_ m / k ]_ B )
105 csbeq1 
 |-  ( n = z -> [_ n / k ]_ B = [_ z / k ]_ B )
106 104 105 disji 
 |-  ( ( Disj_ n e. ( y u. { z } ) [_ n / k ]_ B /\ ( m e. ( y u. { z } ) /\ z e. ( y u. { z } ) ) /\ ( w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> m = z )
107 97 100 101 102 103 106 syl122anc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> m = z )
108 107 98 eqeltrrd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ ( m e. y /\ w e. [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) ) -> z e. y )
109 108 3exp2 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( m e. y -> ( w e. [_ m / k ]_ B -> ( w e. [_ z / k ]_ B -> z e. y ) ) ) )
110 109 rexlimdv 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( E. m e. y w e. [_ m / k ]_ B -> ( w e. [_ z / k ]_ B -> z e. y ) ) )
111 91 110 biimtrid 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( w e. U_ m e. y [_ m / k ]_ B -> ( w e. [_ z / k ]_ B -> z e. y ) ) )
112 111 impd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( ( w e. U_ m e. y [_ m / k ]_ B /\ w e. [_ z / k ]_ B ) -> z e. y ) )
113 90 112 biimtrid 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( w e. ( U_ m e. y [_ m / k ]_ B i^i [_ z / k ]_ B ) -> z e. y ) )
114 89 113 mtod 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> -. w e. ( U_ m e. y [_ m / k ]_ B i^i [_ z / k ]_ B ) )
115 114 eq0rdv 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( U_ m e. y [_ m / k ]_ B i^i [_ z / k ]_ B ) = (/) )
116 mblvol 
 |-  ( U_ m e. y [_ m / k ]_ B e. dom vol -> ( vol ` U_ m e. y [_ m / k ]_ B ) = ( vol* ` U_ m e. y [_ m / k ]_ B ) )
117 71 116 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( vol ` U_ m e. y [_ m / k ]_ B ) = ( vol* ` U_ m e. y [_ m / k ]_ B ) )
118 nfv 
 |-  F/ m ( B e. dom vol /\ ( vol ` B ) e. RR )
119 59 nfel1 
 |-  F/ k [_ m / k ]_ B e. dom vol
120 77 59 nffv 
 |-  F/_ k ( vol ` [_ m / k ]_ B )
121 120 nfel1 
 |-  F/ k ( vol ` [_ m / k ]_ B ) e. RR
122 119 121 nfan 
 |-  F/ k ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR )
123 60 eleq1d 
 |-  ( k = m -> ( B e. dom vol <-> [_ m / k ]_ B e. dom vol ) )
124 60 fveq2d 
 |-  ( k = m -> ( vol ` B ) = ( vol ` [_ m / k ]_ B ) )
125 124 eleq1d 
 |-  ( k = m -> ( ( vol ` B ) e. RR <-> ( vol ` [_ m / k ]_ B ) e. RR ) )
126 123 125 anbi12d 
 |-  ( k = m -> ( ( B e. dom vol /\ ( vol ` B ) e. RR ) <-> ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR ) ) )
127 118 122 126 cbvralw 
 |-  ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) <-> A. m e. ( y u. { z } ) ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR ) )
128 63 127 sylib 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> A. m e. ( y u. { z } ) ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR ) )
129 128 r19.21bi 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ m e. ( y u. { z } ) ) -> ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR ) )
130 129 simpld 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ m e. ( y u. { z } ) ) -> [_ m / k ]_ B e. dom vol )
131 mblss 
 |-  ( [_ m / k ]_ B e. dom vol -> [_ m / k ]_ B C_ RR )
132 130 131 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ m e. ( y u. { z } ) ) -> [_ m / k ]_ B C_ RR )
133 99 132 sylan2 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ m e. y ) -> [_ m / k ]_ B C_ RR )
134 133 ralrimiva 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> A. m e. y [_ m / k ]_ B C_ RR )
135 iunss 
 |-  ( U_ m e. y [_ m / k ]_ B C_ RR <-> A. m e. y [_ m / k ]_ B C_ RR )
136 134 135 sylibr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> U_ m e. y [_ m / k ]_ B C_ RR )
137 mblvol 
 |-  ( [_ m / k ]_ B e. dom vol -> ( vol ` [_ m / k ]_ B ) = ( vol* ` [_ m / k ]_ B ) )
138 137 eleq1d 
 |-  ( [_ m / k ]_ B e. dom vol -> ( ( vol ` [_ m / k ]_ B ) e. RR <-> ( vol* ` [_ m / k ]_ B ) e. RR ) )
139 138 biimpa 
 |-  ( ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR ) -> ( vol* ` [_ m / k ]_ B ) e. RR )
140 129 139 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ m e. ( y u. { z } ) ) -> ( vol* ` [_ m / k ]_ B ) e. RR )
141 99 140 sylan2 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ m e. y ) -> ( vol* ` [_ m / k ]_ B ) e. RR )
142 62 141 fsumrecl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> sum_ m e. y ( vol* ` [_ m / k ]_ B ) e. RR )
143 131 adantr 
 |-  ( ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR ) -> [_ m / k ]_ B C_ RR )
144 143 139 jca 
 |-  ( ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR ) -> ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) )
145 144 ralimi 
 |-  ( A. m e. ( y u. { z } ) ( [_ m / k ]_ B e. dom vol /\ ( vol ` [_ m / k ]_ B ) e. RR ) -> A. m e. ( y u. { z } ) ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) )
146 128 145 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> A. m e. ( y u. { z } ) ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) )
147 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. m e. ( y u. { z } ) ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) -> A. m e. y ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) ) )
148 43 146 147 mpsyl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> A. m e. y ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) )
149 ovolfiniun 
 |-  ( ( y e. Fin /\ A. m e. y ( [_ m / k ]_ B C_ RR /\ ( vol* ` [_ m / k ]_ B ) e. RR ) ) -> ( vol* ` U_ m e. y [_ m / k ]_ B ) <_ sum_ m e. y ( vol* ` [_ m / k ]_ B ) )
150 62 148 149 syl2anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( vol* ` U_ m e. y [_ m / k ]_ B ) <_ sum_ m e. y ( vol* ` [_ m / k ]_ B ) )
151 ovollecl 
 |-  ( ( U_ m e. y [_ m / k ]_ B C_ RR /\ sum_ m e. y ( vol* ` [_ m / k ]_ B ) e. RR /\ ( vol* ` U_ m e. y [_ m / k ]_ B ) <_ sum_ m e. y ( vol* ` [_ m / k ]_ B ) ) -> ( vol* ` U_ m e. y [_ m / k ]_ B ) e. RR )
152 136 142 150 151 syl3anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( vol* ` U_ m e. y [_ m / k ]_ B ) e. RR )
153 117 152 eqeltrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( vol ` U_ m e. y [_ m / k ]_ B ) e. RR )
154 87 simprd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( vol ` [_ z / k ]_ B ) e. RR )
155 volun 
 |-  ( ( ( U_ m e. y [_ m / k ]_ B e. dom vol /\ [_ z / k ]_ B e. dom vol /\ ( U_ m e. y [_ m / k ]_ B i^i [_ z / k ]_ B ) = (/) ) /\ ( ( vol ` U_ m e. y [_ m / k ]_ B ) e. RR /\ ( vol ` [_ z / k ]_ B ) e. RR ) ) -> ( vol ` ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B ) ) = ( ( vol ` U_ m e. y [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) )
156 71 88 115 153 154 155 syl32anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( vol ` ( U_ m e. y [_ m / k ]_ B u. [_ z / k ]_ B ) ) = ( ( vol ` U_ m e. y [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) )
157 57 156 eqtrid 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( vol ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) = ( ( vol ` U_ m e. y [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) )
158 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
159 89 158 sylibr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( y i^i { z } ) = (/) )
160 eqidd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( y u. { z } ) = ( y u. { z } ) )
161 snfi 
 |-  { z } e. Fin
162 unfi 
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
163 62 161 162 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( y u. { z } ) e. Fin )
164 129 simprd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ m e. ( y u. { z } ) ) -> ( vol ` [_ m / k ]_ B ) e. RR )
165 164 recnd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) /\ m e. ( y u. { z } ) ) -> ( vol ` [_ m / k ]_ B ) e. CC )
166 159 160 163 165 fsumsplit 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> sum_ m e. ( y u. { z } ) ( vol ` [_ m / k ]_ B ) = ( sum_ m e. y ( vol ` [_ m / k ]_ B ) + sum_ m e. { z } ( vol ` [_ m / k ]_ B ) ) )
167 154 recnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( vol ` [_ z / k ]_ B ) e. CC )
168 53 fveq2d 
 |-  ( m = z -> ( vol ` [_ m / k ]_ B ) = ( vol ` [_ z / k ]_ B ) )
169 168 sumsn 
 |-  ( ( z e. _V /\ ( vol ` [_ z / k ]_ B ) e. CC ) -> sum_ m e. { z } ( vol ` [_ m / k ]_ B ) = ( vol ` [_ z / k ]_ B ) )
170 52 167 169 sylancr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> sum_ m e. { z } ( vol ` [_ m / k ]_ B ) = ( vol ` [_ z / k ]_ B ) )
171 170 oveq2d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( sum_ m e. y ( vol ` [_ m / k ]_ B ) + sum_ m e. { z } ( vol ` [_ m / k ]_ B ) ) = ( sum_ m e. y ( vol ` [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) )
172 166 171 eqtrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> sum_ m e. ( y u. { z } ) ( vol ` [_ m / k ]_ B ) = ( sum_ m e. y ( vol ` [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) )
173 157 172 eqeq12d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( ( vol ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) = sum_ m e. ( y u. { z } ) ( vol ` [_ m / k ]_ B ) <-> ( ( vol ` U_ m e. y [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) = ( sum_ m e. y ( vol ` [_ m / k ]_ B ) + ( vol ` [_ z / k ]_ B ) ) ) )
174 50 173 imbitrrid 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( ( vol ` U_ m e. y [_ m / k ]_ B ) = sum_ m e. y ( vol ` [_ m / k ]_ B ) -> ( vol ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) = sum_ m e. ( y u. { z } ) ( vol ` [_ m / k ]_ B ) ) )
175 61 fveq2i 
 |-  ( vol ` U_ k e. y B ) = ( vol ` U_ m e. y [_ m / k ]_ B )
176 nfcv 
 |-  F/_ m ( vol ` B )
177 124 176 120 cbvsum 
 |-  sum_ k e. y ( vol ` B ) = sum_ m e. y ( vol ` [_ m / k ]_ B )
178 175 177 eqeq12i 
 |-  ( ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) <-> ( vol ` U_ m e. y [_ m / k ]_ B ) = sum_ m e. y ( vol ` [_ m / k ]_ B ) )
179 58 59 60 cbviun 
 |-  U_ k e. ( y u. { z } ) B = U_ m e. ( y u. { z } ) [_ m / k ]_ B
180 179 fveq2i 
 |-  ( vol ` U_ k e. ( y u. { z } ) B ) = ( vol ` U_ m e. ( y u. { z } ) [_ m / k ]_ B )
181 124 176 120 cbvsum 
 |-  sum_ k e. ( y u. { z } ) ( vol ` B ) = sum_ m e. ( y u. { z } ) ( vol ` [_ m / k ]_ B )
182 180 181 eqeq12i 
 |-  ( ( vol ` U_ k e. ( y u. { z } ) B ) = sum_ k e. ( y u. { z } ) ( vol ` B ) <-> ( vol ` U_ m e. ( y u. { z } ) [_ m / k ]_ B ) = sum_ m e. ( y u. { z } ) ( vol ` [_ m / k ]_ B ) )
183 174 178 182 3imtr4g 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) ) -> ( ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) -> ( vol ` U_ k e. ( y u. { z } ) B ) = sum_ k e. ( y u. { z } ) ( vol ` B ) ) )
184 183 ex 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) -> ( ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) -> ( vol ` U_ k e. ( y u. { z } ) B ) = sum_ k e. ( y u. { z } ) ( vol ` B ) ) ) )
185 184 a2d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) -> ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) ) -> ( ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) -> ( vol ` U_ k e. ( y u. { z } ) B ) = sum_ k e. ( y u. { z } ) ( vol ` B ) ) ) )
186 49 185 syl5 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( A. k e. y ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. y B ) -> ( vol ` U_ k e. y B ) = sum_ k e. y ( vol ` B ) ) -> ( ( A. k e. ( y u. { z } ) ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. ( y u. { z } ) B ) -> ( vol ` U_ k e. ( y u. { z } ) B ) = sum_ k e. ( y u. { z } ) ( vol ` B ) ) ) )
187 8 16 24 32 42 186 findcard2s 
 |-  ( A e. Fin -> ( ( A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. A B ) -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) ) )
188 187 3impib 
 |-  ( ( A e. Fin /\ A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. A B ) -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) )