MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unmbl Structured version   Unicode version

Theorem unmbl 21034
Description: A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
Assertion
Ref Expression
unmbl  |-  ( ( A  e.  dom  vol  /\  B  e.  dom  vol )  ->  ( A  u.  B )  e.  dom  vol )

Proof of Theorem unmbl
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 mblss 21029 . . . 4  |-  ( A  e.  dom  vol  ->  A 
C_  RR )
2 mblss 21029 . . . 4  |-  ( B  e.  dom  vol  ->  B 
C_  RR )
31, 2anim12i 566 . . 3  |-  ( ( A  e.  dom  vol  /\  B  e.  dom  vol )  ->  ( A  C_  RR  /\  B  C_  RR ) )
4 unss 3545 . . 3  |-  ( ( A  C_  RR  /\  B  C_  RR )  <->  ( A  u.  B )  C_  RR )
53, 4sylib 196 . 2  |-  ( ( A  e.  dom  vol  /\  B  e.  dom  vol )  ->  ( A  u.  B )  C_  RR )
6 elpwi 3884 . . . 4  |-  ( x  e.  ~P RR  ->  x 
C_  RR )
7 inss1 3585 . . . . . . . . 9  |-  ( x  i^i  ( A  u.  B ) )  C_  x
8 ovolsscl 20984 . . . . . . . . 9  |-  ( ( ( x  i^i  ( A  u.  B )
)  C_  x  /\  x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  ( x  i^i  ( A  u.  B )
) )  e.  RR )
97, 8mp3an1 1301 . . . . . . . 8  |-  ( ( x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  ( x  i^i  ( A  u.  B )
) )  e.  RR )
109adantl 466 . . . . . . 7  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  i^i  ( A  u.  B )
) )  e.  RR )
11 inss1 3585 . . . . . . . . . 10  |-  ( x  i^i  A )  C_  x
12 ovolsscl 20984 . . . . . . . . . 10  |-  ( ( ( x  i^i  A
)  C_  x  /\  x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  ( x  i^i  A ) )  e.  RR )
1311, 12mp3an1 1301 . . . . . . . . 9  |-  ( ( x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  ( x  i^i  A ) )  e.  RR )
1413adantl 466 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  i^i  A
) )  e.  RR )
15 difss 3498 . . . . . . . . . 10  |-  ( x 
\  A )  C_  x
16 simprl 755 . . . . . . . . . 10  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  x  C_  RR )
1715, 16syl5ss 3382 . . . . . . . . 9  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( x  \  A )  C_  RR )
18 ovolsscl 20984 . . . . . . . . . . 11  |-  ( ( ( x  \  A
)  C_  x  /\  x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  ( x  \  A ) )  e.  RR )
1915, 18mp3an1 1301 . . . . . . . . . 10  |-  ( ( x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  ( x  \  A ) )  e.  RR )
2019adantl 466 . . . . . . . . 9  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  \  A
) )  e.  RR )
21 inss1 3585 . . . . . . . . . 10  |-  ( ( x  \  A )  i^i  B )  C_  ( x  \  A )
22 ovolsscl 20984 . . . . . . . . . 10  |-  ( ( ( ( x  \  A )  i^i  B
)  C_  ( x  \  A )  /\  (
x  \  A )  C_  RR  /\  ( vol* `  ( x  \  A ) )  e.  RR )  ->  ( vol* `  ( ( x  \  A )  i^i  B ) )  e.  RR )
2321, 22mp3an1 1301 . . . . . . . . 9  |-  ( ( ( x  \  A
)  C_  RR  /\  ( vol* `  ( x 
\  A ) )  e.  RR )  -> 
( vol* `  ( ( x  \  A )  i^i  B
) )  e.  RR )
2417, 20, 23syl2anc 661 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( ( x  \  A )  i^i  B
) )  e.  RR )
2514, 24readdcld 9428 . . . . . . 7  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( ( vol* `  ( x  i^i  A ) )  +  ( vol* `  ( ( x  \  A )  i^i  B
) ) )  e.  RR )
26 difss 3498 . . . . . . . . 9  |-  ( x 
\  ( A  u.  B ) )  C_  x
27 ovolsscl 20984 . . . . . . . . 9  |-  ( ( ( x  \  ( A  u.  B )
)  C_  x  /\  x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  ( x  \  ( A  u.  B )
) )  e.  RR )
2826, 27mp3an1 1301 . . . . . . . 8  |-  ( ( x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  ( x  \  ( A  u.  B )
) )  e.  RR )
2928adantl 466 . . . . . . 7  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  \  ( A  u.  B )
) )  e.  RR )
30 incom 3558 . . . . . . . . . . . 12  |-  ( ( x  \  A )  i^i  B )  =  ( B  i^i  (
x  \  A )
)
31 indifcom 3610 . . . . . . . . . . . 12  |-  ( B  i^i  ( x  \  A ) )  =  ( x  i^i  ( B  \  A ) )
3230, 31eqtri 2463 . . . . . . . . . . 11  |-  ( ( x  \  A )  i^i  B )  =  ( x  i^i  ( B  \  A ) )
3332uneq2i 3522 . . . . . . . . . 10  |-  ( ( x  i^i  A )  u.  ( ( x 
\  A )  i^i 
B ) )  =  ( ( x  i^i 
A )  u.  (
x  i^i  ( B  \  A ) ) )
34 indi 3611 . . . . . . . . . 10  |-  ( x  i^i  ( A  u.  ( B  \  A ) ) )  =  ( ( x  i^i  A
)  u.  ( x  i^i  ( B  \  A ) ) )
35 undif2 3770 . . . . . . . . . . 11  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
3635ineq2i 3564 . . . . . . . . . 10  |-  ( x  i^i  ( A  u.  ( B  \  A ) ) )  =  ( x  i^i  ( A  u.  B ) )
3733, 34, 363eqtr2ri 2470 . . . . . . . . 9  |-  ( x  i^i  ( A  u.  B ) )  =  ( ( x  i^i 
A )  u.  (
( x  \  A
)  i^i  B )
)
3837fveq2i 5709 . . . . . . . 8  |-  ( vol* `  ( x  i^i  ( A  u.  B
) ) )  =  ( vol* `  ( ( x  i^i 
A )  u.  (
( x  \  A
)  i^i  B )
) )
3911, 16syl5ss 3382 . . . . . . . . 9  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( x  i^i 
A )  C_  RR )
4021, 17syl5ss 3382 . . . . . . . . 9  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( ( x 
\  A )  i^i 
B )  C_  RR )
41 ovolun 20997 . . . . . . . . 9  |-  ( ( ( ( x  i^i 
A )  C_  RR  /\  ( vol* `  ( x  i^i  A ) )  e.  RR )  /\  ( ( ( x  \  A )  i^i  B )  C_  RR  /\  ( vol* `  ( ( x  \  A )  i^i  B
) )  e.  RR ) )  ->  ( vol* `  ( ( x  i^i  A )  u.  ( ( x 
\  A )  i^i 
B ) ) )  <_  ( ( vol* `  ( x  i^i  A ) )  +  ( vol* `  ( ( x  \  A )  i^i  B
) ) ) )
4239, 14, 40, 24, 41syl22anc 1219 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( ( x  i^i 
A )  u.  (
( x  \  A
)  i^i  B )
) )  <_  (
( vol* `  ( x  i^i  A ) )  +  ( vol* `  ( (
x  \  A )  i^i  B ) ) ) )
4338, 42syl5eqbr 4340 . . . . . . 7  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  i^i  ( A  u.  B )
) )  <_  (
( vol* `  ( x  i^i  A ) )  +  ( vol* `  ( (
x  \  A )  i^i  B ) ) ) )
4410, 25, 29, 43leadd1dd 9968 . . . . . 6  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( ( vol* `  ( x  i^i  ( A  u.  B
) ) )  +  ( vol* `  ( x  \  ( A  u.  B )
) ) )  <_ 
( ( ( vol* `  ( x  i^i  A ) )  +  ( vol* `  ( ( x  \  A )  i^i  B
) ) )  +  ( vol* `  ( x  \  ( A  u.  B )
) ) ) )
45 simplr 754 . . . . . . . . . 10  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  B  e.  dom  vol )
46 mblsplit 21030 . . . . . . . . . 10  |-  ( ( B  e.  dom  vol  /\  ( x  \  A
)  C_  RR  /\  ( vol* `  ( x 
\  A ) )  e.  RR )  -> 
( vol* `  ( x  \  A ) )  =  ( ( vol* `  (
( x  \  A
)  i^i  B )
)  +  ( vol* `  ( (
x  \  A )  \  B ) ) ) )
4745, 17, 20, 46syl3anc 1218 . . . . . . . . 9  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  \  A
) )  =  ( ( vol* `  ( ( x  \  A )  i^i  B
) )  +  ( vol* `  (
( x  \  A
)  \  B )
) ) )
48 difun1 3625 . . . . . . . . . . 11  |-  ( x 
\  ( A  u.  B ) )  =  ( ( x  \  A )  \  B
)
4948fveq2i 5709 . . . . . . . . . 10  |-  ( vol* `  ( x  \  ( A  u.  B
) ) )  =  ( vol* `  ( ( x  \  A )  \  B
) )
5049oveq2i 6117 . . . . . . . . 9  |-  ( ( vol* `  (
( x  \  A
)  i^i  B )
)  +  ( vol* `  ( x  \  ( A  u.  B
) ) ) )  =  ( ( vol* `  ( (
x  \  A )  i^i  B ) )  +  ( vol* `  ( ( x  \  A )  \  B
) ) )
5147, 50syl6eqr 2493 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  \  A
) )  =  ( ( vol* `  ( ( x  \  A )  i^i  B
) )  +  ( vol* `  (
x  \  ( A  u.  B ) ) ) ) )
5251oveq2d 6122 . . . . . . 7  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( ( vol* `  ( x  i^i  A ) )  +  ( vol* `  ( x  \  A ) ) )  =  ( ( vol* `  ( x  i^i  A ) )  +  ( ( vol* `  (
( x  \  A
)  i^i  B )
)  +  ( vol* `  ( x  \  ( A  u.  B
) ) ) ) ) )
53 simpll 753 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  A  e.  dom  vol )
54 simprr 756 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  x )  e.  RR )
55 mblsplit 21030 . . . . . . . 8  |-  ( ( A  e.  dom  vol  /\  x  C_  RR  /\  ( vol* `  x )  e.  RR )  -> 
( vol* `  x )  =  ( ( vol* `  ( x  i^i  A ) )  +  ( vol* `  ( x  \  A ) ) ) )
5653, 16, 54, 55syl3anc 1218 . . . . . . 7  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  x )  =  ( ( vol* `  ( x  i^i  A ) )  +  ( vol* `  ( x  \  A ) ) ) )
5714recnd 9427 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  i^i  A
) )  e.  CC )
5824recnd 9427 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( ( x  \  A )  i^i  B
) )  e.  CC )
5929recnd 9427 . . . . . . . 8  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  ( x  \  ( A  u.  B )
) )  e.  CC )
6057, 58, 59addassd 9423 . . . . . . 7  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( ( ( vol* `  (
x  i^i  A )
)  +  ( vol* `  ( (
x  \  A )  i^i  B ) ) )  +  ( vol* `  ( x  \  ( A  u.  B )
) ) )  =  ( ( vol* `  ( x  i^i  A
) )  +  ( ( vol* `  ( ( x  \  A )  i^i  B
) )  +  ( vol* `  (
x  \  ( A  u.  B ) ) ) ) ) )
6152, 56, 603eqtr4d 2485 . . . . . 6  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( vol* `  x )  =  ( ( ( vol* `  ( x  i^i  A
) )  +  ( vol* `  (
( x  \  A
)  i^i  B )
) )  +  ( vol* `  (
x  \  ( A  u.  B ) ) ) ) )
6244, 61breqtrrd 4333 . . . . 5  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  ( x 
C_  RR  /\  ( vol* `  x )  e.  RR ) )  ->  ( ( vol* `  ( x  i^i  ( A  u.  B
) ) )  +  ( vol* `  ( x  \  ( A  u.  B )
) ) )  <_ 
( vol* `  x ) )
6362expr 615 . . . 4  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  x  C_  RR )  ->  ( ( vol* `  x
)  e.  RR  ->  ( ( vol* `  ( x  i^i  ( A  u.  B )
) )  +  ( vol* `  (
x  \  ( A  u.  B ) ) ) )  <_  ( vol* `  x ) ) )
646, 63sylan2 474 . . 3  |-  ( ( ( A  e.  dom  vol 
/\  B  e.  dom  vol )  /\  x  e. 
~P RR )  -> 
( ( vol* `  x )  e.  RR  ->  ( ( vol* `  ( x  i^i  ( A  u.  B )
) )  +  ( vol* `  (
x  \  ( A  u.  B ) ) ) )  <_  ( vol* `  x ) ) )
6564ralrimiva 2814 . 2  |-  ( ( A  e.  dom  vol  /\  B  e.  dom  vol )  ->  A. x  e.  ~P  RR ( ( vol* `  x )  e.  RR  ->  ( ( vol* `  ( x  i^i  ( A  u.  B )
) )  +  ( vol* `  (
x  \  ( A  u.  B ) ) ) )  <_  ( vol* `  x ) ) )
66 ismbl2 21025 . 2  |-  ( ( A  u.  B )  e.  dom  vol  <->  ( ( A  u.  B )  C_  RR  /\  A. x  e.  ~P  RR ( ( vol* `  x
)  e.  RR  ->  ( ( vol* `  ( x  i^i  ( A  u.  B )
) )  +  ( vol* `  (
x  \  ( A  u.  B ) ) ) )  <_  ( vol* `  x ) ) ) )
675, 65, 66sylanbrc 664 1  |-  ( ( A  e.  dom  vol  /\  B  e.  dom  vol )  ->  ( A  u.  B )  e.  dom  vol )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2730    \ cdif 3340    u. cun 3341    i^i cin 3342    C_ wss 3343   ~Pcpw 3875   class class class wbr 4307   dom cdm 4855   ` cfv 5433  (class class class)co 6106   RRcr 9296    + caddc 9300    <_ cle 9434   vol*covol 20961   volcvol 20962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374  ax-pre-sup 9375
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-om 6492  df-1st 6592  df-2nd 6593  df-recs 6847  df-rdg 6881  df-er 7116  df-map 7231  df-en 7326  df-dom 7327  df-sdom 7328  df-sup 7706  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-div 10009  df-nn 10338  df-2 10395  df-3 10396  df-n0 10595  df-z 10662  df-uz 10877  df-q 10969  df-rp 11007  df-ioo 11319  df-ico 11321  df-icc 11322  df-fz 11453  df-fl 11657  df-seq 11822  df-exp 11881  df-cj 12603  df-re 12604  df-im 12605  df-sqr 12739  df-abs 12740  df-ovol 20963  df-vol 20964
This theorem is referenced by:  inmbl  21038  finiunmbl  21040  volun  21041  voliunlem1  21046  icombl1  21059  iccmbl  21062  uniiccmbl  21085  mbfimaicc  21126  mbfeqalem  21135  mbfres2  21138  mbfmax  21142  itgss3  21307  ismblfin  28451  mbfposadd  28458  cnambfre  28459  itg2addnclem2  28463  iblabsnclem  28474  ftc1anclem1  28486  ftc1anclem5  28490  iocmbl  29607
  Copyright terms: Public domain W3C validator