Metamath Proof Explorer

Theorem measvunilem

Description: Lemma for measvuni . (Contributed by Thierry Arnoux, 7-Feb-2017) (Revised by Thierry Arnoux, 19-Feb-2017) (Revised by Thierry Arnoux, 6-Mar-2017)

Ref Expression
Hypothesis measvunilem.1 
|- F/_ x A
Assertion measvunilem 
|- ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = sum* x e. A ( M ` B ) )

Proof

Step Hyp Ref Expression
1 measvunilem.1 
 |-  F/_ x A
2 simp1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> M e. ( measures ` S ) )
3 simp3l 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A ~<_ _om )
4 1 abrexctf 
 |-  ( A ~<_ _om -> { y | E. x e. A y = B } ~<_ _om )
5 3 4 syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { y | E. x e. A y = B } ~<_ _om )
6 ctex 
 |-  ( { y | E. x e. A y = B } ~<_ _om -> { y | E. x e. A y = B } e. _V )
7 5 6 syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { y | E. x e. A y = B } e. _V )
8 simp2 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A. x e. A B e. ( S \ { (/) } ) )
9 eldifi 
 |-  ( B e. ( S \ { (/) } ) -> B e. S )
10 9 ralimi 
 |-  ( A. x e. A B e. ( S \ { (/) } ) -> A. x e. A B e. S )
11 nfcv 
 |-  F/_ x S
12 11 abrexss 
 |-  ( A. x e. A B e. S -> { y | E. x e. A y = B } C_ S )
13 10 12 syl 
 |-  ( A. x e. A B e. ( S \ { (/) } ) -> { y | E. x e. A y = B } C_ S )
14 8 13 syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { y | E. x e. A y = B } C_ S )
15 elpwg 
 |-  ( { y | E. x e. A y = B } e. _V -> ( { y | E. x e. A y = B } e. ~P S <-> { y | E. x e. A y = B } C_ S ) )
16 15 biimpar 
 |-  ( ( { y | E. x e. A y = B } e. _V /\ { y | E. x e. A y = B } C_ S ) -> { y | E. x e. A y = B } e. ~P S )
17 7 14 16 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> { y | E. x e. A y = B } e. ~P S )
18 simp3r 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> Disj_ x e. A B )
19 1 disjabrexf 
 |-  ( Disj_ x e. A B -> Disj_ z e. { y | E. x e. A y = B } z )
20 18 19 syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> Disj_ z e. { y | E. x e. A y = B } z )
21 measvun 
 |-  ( ( M e. ( measures ` S ) /\ { y | E. x e. A y = B } e. ~P S /\ ( { y | E. x e. A y = B } ~<_ _om /\ Disj_ z e. { y | E. x e. A y = B } z ) ) -> ( M ` U. { y | E. x e. A y = B } ) = sum* z e. { y | E. x e. A y = B } ( M ` z ) )
22 2 17 5 20 21 syl112anc 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U. { y | E. x e. A y = B } ) = sum* z e. { y | E. x e. A y = B } ( M ` z ) )
23 dfiun2g 
 |-  ( A. x e. A B e. ( S \ { (/) } ) -> U_ x e. A B = U. { y | E. x e. A y = B } )
24 23 fveq2d 
 |-  ( A. x e. A B e. ( S \ { (/) } ) -> ( M ` U_ x e. A B ) = ( M ` U. { y | E. x e. A y = B } ) )
25 8 24 syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = ( M ` U. { y | E. x e. A y = B } ) )
26 nfcv 
 |-  F/_ x ( M ` z )
27 nfv 
 |-  F/ x M e. ( measures ` S )
28 nfra1 
 |-  F/ x A. x e. A B e. ( S \ { (/) } )
29 nfcv 
 |-  F/_ x ~<_
30 nfcv 
 |-  F/_ x _om
31 1 29 30 nfbr 
 |-  F/ x A ~<_ _om
32 nfdisj1 
 |-  F/ x Disj_ x e. A B
33 31 32 nfan 
 |-  F/ x ( A ~<_ _om /\ Disj_ x e. A B )
34 27 28 33 nf3an 
 |-  F/ x ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) )
35 fveq2 
 |-  ( z = B -> ( M ` z ) = ( M ` B ) )
36 ctex 
 |-  ( A ~<_ _om -> A e. _V )
37 3 36 syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A e. _V )
38 8 r19.21bi 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. A ) -> B e. ( S \ { (/) } ) )
39 34 1 38 18 disjdsct 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> Fun `' ( x e. A |-> B ) )
40 simpl1 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. A ) -> M e. ( measures ` S ) )
41 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ B e. S ) -> ( M ` B ) e. ( 0 [,] +oo ) )
42 9 41 sylan2 
 |-  ( ( M e. ( measures ` S ) /\ B e. ( S \ { (/) } ) ) -> ( M ` B ) e. ( 0 [,] +oo ) )
43 40 38 42 syl2anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. A ) -> ( M ` B ) e. ( 0 [,] +oo ) )
44 26 34 1 35 37 39 43 38 esumc 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> sum* x e. A ( M ` B ) = sum* z e. { y | E. x e. A y = B } ( M ` z ) )
45 22 25 44 3eqtr4d 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = sum* x e. A ( M ` B ) )