Step |
Hyp |
Ref |
Expression |
1 |
|
itg1addlem.1 |
|- ( ph -> F : X --> Y ) |
2 |
|
itg1addlem.2 |
|- ( ph -> A e. Fin ) |
3 |
|
itg1addlem.3 |
|- ( ( ph /\ k e. A ) -> B C_ ( `' F " { k } ) ) |
4 |
|
itg1addlem.4 |
|- ( ( ph /\ k e. A ) -> B e. dom vol ) |
5 |
|
itg1addlem.5 |
|- ( ( ph /\ k e. A ) -> ( vol ` B ) e. RR ) |
6 |
4 5
|
jca |
|- ( ( ph /\ k e. A ) -> ( B e. dom vol /\ ( vol ` B ) e. RR ) ) |
7 |
6
|
ralrimiva |
|- ( ph -> A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) ) |
8 |
3
|
adantrr |
|- ( ( ph /\ ( k e. A /\ x e. B ) ) -> B C_ ( `' F " { k } ) ) |
9 |
|
simprr |
|- ( ( ph /\ ( k e. A /\ x e. B ) ) -> x e. B ) |
10 |
8 9
|
sseldd |
|- ( ( ph /\ ( k e. A /\ x e. B ) ) -> x e. ( `' F " { k } ) ) |
11 |
1
|
ffnd |
|- ( ph -> F Fn X ) |
12 |
11
|
adantr |
|- ( ( ph /\ ( k e. A /\ x e. B ) ) -> F Fn X ) |
13 |
|
fniniseg |
|- ( F Fn X -> ( x e. ( `' F " { k } ) <-> ( x e. X /\ ( F ` x ) = k ) ) ) |
14 |
12 13
|
syl |
|- ( ( ph /\ ( k e. A /\ x e. B ) ) -> ( x e. ( `' F " { k } ) <-> ( x e. X /\ ( F ` x ) = k ) ) ) |
15 |
10 14
|
mpbid |
|- ( ( ph /\ ( k e. A /\ x e. B ) ) -> ( x e. X /\ ( F ` x ) = k ) ) |
16 |
15
|
simprd |
|- ( ( ph /\ ( k e. A /\ x e. B ) ) -> ( F ` x ) = k ) |
17 |
16
|
ralrimivva |
|- ( ph -> A. k e. A A. x e. B ( F ` x ) = k ) |
18 |
|
invdisj |
|- ( A. k e. A A. x e. B ( F ` x ) = k -> Disj_ k e. A B ) |
19 |
17 18
|
syl |
|- ( ph -> Disj_ k e. A B ) |
20 |
|
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 ) ) |
21 |
2 7 19 20
|
syl3anc |
|- ( ph -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) ) |