Metamath Proof Explorer

Theorem finiunmbl

Description: A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Assertion finiunmbl 
|- ( ( A e. Fin /\ A. k e. A B e. dom vol ) -> U_ k e. A B e. dom vol )

Proof

Step Hyp Ref Expression
1 raleq 
 |-  ( y = (/) -> ( A. k e. y B e. dom vol <-> A. k e. (/) B e. dom vol ) )
2 iuneq1 
 |-  ( y = (/) -> U_ k e. y B = U_ k e. (/) B )
3 2 eleq1d 
 |-  ( y = (/) -> ( U_ k e. y B e. dom vol <-> U_ k e. (/) B e. dom vol ) )
4 1 3 imbi12d 
 |-  ( y = (/) -> ( ( A. k e. y B e. dom vol -> U_ k e. y B e. dom vol ) <-> ( A. k e. (/) B e. dom vol -> U_ k e. (/) B e. dom vol ) ) )
5 raleq 
 |-  ( y = x -> ( A. k e. y B e. dom vol <-> A. k e. x B e. dom vol ) )
6 iuneq1 
 |-  ( y = x -> U_ k e. y B = U_ k e. x B )
7 6 eleq1d 
 |-  ( y = x -> ( U_ k e. y B e. dom vol <-> U_ k e. x B e. dom vol ) )
8 5 7 imbi12d 
 |-  ( y = x -> ( ( A. k e. y B e. dom vol -> U_ k e. y B e. dom vol ) <-> ( A. k e. x B e. dom vol -> U_ k e. x B e. dom vol ) ) )
9 raleq 
 |-  ( y = ( x u. { z } ) -> ( A. k e. y B e. dom vol <-> A. k e. ( x u. { z } ) B e. dom vol ) )
10 iuneq1 
 |-  ( y = ( x u. { z } ) -> U_ k e. y B = U_ k e. ( x u. { z } ) B )
11 10 eleq1d 
 |-  ( y = ( x u. { z } ) -> ( U_ k e. y B e. dom vol <-> U_ k e. ( x u. { z } ) B e. dom vol ) )
12 9 11 imbi12d 
 |-  ( y = ( x u. { z } ) -> ( ( A. k e. y B e. dom vol -> U_ k e. y B e. dom vol ) <-> ( A. k e. ( x u. { z } ) B e. dom vol -> U_ k e. ( x u. { z } ) B e. dom vol ) ) )
13 raleq 
 |-  ( y = A -> ( A. k e. y B e. dom vol <-> A. k e. A B e. dom vol ) )
14 iuneq1 
 |-  ( y = A -> U_ k e. y B = U_ k e. A B )
15 14 eleq1d 
 |-  ( y = A -> ( U_ k e. y B e. dom vol <-> U_ k e. A B e. dom vol ) )
16 13 15 imbi12d 
 |-  ( y = A -> ( ( A. k e. y B e. dom vol -> U_ k e. y B e. dom vol ) <-> ( A. k e. A B e. dom vol -> U_ k e. A B e. dom vol ) ) )
17 0iun 
 |-  U_ k e. (/) B = (/)
18 0mbl 
 |-  (/) e. dom vol
19 17 18 eqeltri 
 |-  U_ k e. (/) B e. dom vol
20 19 a1i 
 |-  ( A. k e. (/) B e. dom vol -> U_ k e. (/) B e. dom vol )
21 ssun1 
 |-  x C_ ( x u. { z } )
22 ssralv 
 |-  ( x C_ ( x u. { z } ) -> ( A. k e. ( x u. { z } ) B e. dom vol -> A. k e. x B e. dom vol ) )
23 21 22 ax-mp 
 |-  ( A. k e. ( x u. { z } ) B e. dom vol -> A. k e. x B e. dom vol )
24 23 imim1i 
 |-  ( ( A. k e. x B e. dom vol -> U_ k e. x B e. dom vol ) -> ( A. k e. ( x u. { z } ) B e. dom vol -> U_ k e. x B e. dom vol ) )
25 ssun2 
 |-  { z } C_ ( x u. { z } )
26 ssralv 
 |-  ( { z } C_ ( x u. { z } ) -> ( A. k e. ( x u. { z } ) B e. dom vol -> A. k e. { z } B e. dom vol ) )
27 25 26 ax-mp 
 |-  ( A. k e. ( x u. { z } ) B e. dom vol -> A. k e. { z } B e. dom vol )
28 iunxun 
 |-  U_ k e. ( x u. { z } ) B = ( U_ k e. x B u. U_ k e. { z } B )
29 vex 
 |-  z e. _V
30 csbeq1 
 |-  ( x = z -> [_ x / k ]_ B = [_ z / k ]_ B )
31 30 eleq1d 
 |-  ( x = z -> ( [_ x / k ]_ B e. dom vol <-> [_ z / k ]_ B e. dom vol ) )
32 29 31 ralsn 
 |-  ( A. x e. { z } [_ x / k ]_ B e. dom vol <-> [_ z / k ]_ B e. dom vol )
33 nfv 
 |-  F/ x B e. dom vol
34 nfcsb1v 
 |-  F/_ k [_ x / k ]_ B
35 34 nfel1 
 |-  F/ k [_ x / k ]_ B e. dom vol
36 csbeq1a 
 |-  ( k = x -> B = [_ x / k ]_ B )
37 36 eleq1d 
 |-  ( k = x -> ( B e. dom vol <-> [_ x / k ]_ B e. dom vol ) )
38 33 35 37 cbvralw 
 |-  ( A. k e. { z } B e. dom vol <-> A. x e. { z } [_ x / k ]_ B e. dom vol )
39 nfcv 
 |-  F/_ x B
40 39 34 36 cbviun 
 |-  U_ k e. { z } B = U_ x e. { z } [_ x / k ]_ B
41 29 30 iunxsn 
 |-  U_ x e. { z } [_ x / k ]_ B = [_ z / k ]_ B
42 40 41 eqtri 
 |-  U_ k e. { z } B = [_ z / k ]_ B
43 42 eleq1i 
 |-  ( U_ k e. { z } B e. dom vol <-> [_ z / k ]_ B e. dom vol )
44 32 38 43 3bitr4i 
 |-  ( A. k e. { z } B e. dom vol <-> U_ k e. { z } B e. dom vol )
45 unmbl 
 |-  ( ( U_ k e. x B e. dom vol /\ U_ k e. { z } B e. dom vol ) -> ( U_ k e. x B u. U_ k e. { z } B ) e. dom vol )
46 44 45 sylan2b 
 |-  ( ( U_ k e. x B e. dom vol /\ A. k e. { z } B e. dom vol ) -> ( U_ k e. x B u. U_ k e. { z } B ) e. dom vol )
47 28 46 eqeltrid 
 |-  ( ( U_ k e. x B e. dom vol /\ A. k e. { z } B e. dom vol ) -> U_ k e. ( x u. { z } ) B e. dom vol )
48 47 expcom 
 |-  ( A. k e. { z } B e. dom vol -> ( U_ k e. x B e. dom vol -> U_ k e. ( x u. { z } ) B e. dom vol ) )
49 27 48 syl 
 |-  ( A. k e. ( x u. { z } ) B e. dom vol -> ( U_ k e. x B e. dom vol -> U_ k e. ( x u. { z } ) B e. dom vol ) )
50 24 49 sylcom 
 |-  ( ( A. k e. x B e. dom vol -> U_ k e. x B e. dom vol ) -> ( A. k e. ( x u. { z } ) B e. dom vol -> U_ k e. ( x u. { z } ) B e. dom vol ) )
51 50 a1i 
 |-  ( x e. Fin -> ( ( A. k e. x B e. dom vol -> U_ k e. x B e. dom vol ) -> ( A. k e. ( x u. { z } ) B e. dom vol -> U_ k e. ( x u. { z } ) B e. dom vol ) ) )
52 4 8 12 16 20 51 findcard2 
 |-  ( A e. Fin -> ( A. k e. A B e. dom vol -> U_ k e. A B e. dom vol ) )
53 52 imp 
 |-  ( ( A e. Fin /\ A. k e. A B e. dom vol ) -> U_ k e. A B e. dom vol )