Metamath Proof Explorer

Theorem iunmbl

Description: The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion iunmbl 
|- ( A. n e. NN A e. dom vol -> U_ n e. NN A e. dom vol )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ k A e. dom vol
2 nfcsb1v 
 |-  F/_ n [_ k / n ]_ A
3 2 nfel1 
 |-  F/ n [_ k / n ]_ A e. dom vol
4 csbeq1a 
 |-  ( n = k -> A = [_ k / n ]_ A )
5 4 eleq1d 
 |-  ( n = k -> ( A e. dom vol <-> [_ k / n ]_ A e. dom vol ) )
6 1 3 5 cbvralw 
 |-  ( A. n e. NN A e. dom vol <-> A. k e. NN [_ k / n ]_ A e. dom vol )
7 nfcv 
 |-  F/_ k A
8 7 2 4 cbviun 
 |-  U_ n e. NN A = U_ k e. NN [_ k / n ]_ A
9 csbeq1 
 |-  ( k = m -> [_ k / n ]_ A = [_ m / n ]_ A )
10 9 iundisj 
 |-  U_ k e. NN [_ k / n ]_ A = U_ k e. NN ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A )
11 8 10 eqtri 
 |-  U_ n e. NN A = U_ k e. NN ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A )
12 difexg 
 |-  ( [_ k / n ]_ A e. dom vol -> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) e. _V )
13 12 ralimi 
 |-  ( A. k e. NN [_ k / n ]_ A e. dom vol -> A. k e. NN ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) e. _V )
14 dfiun2g 
 |-  ( A. k e. NN ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) e. _V -> U_ k e. NN ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) = U. { y | E. k e. NN y = ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) } )
15 13 14 syl 
 |-  ( A. k e. NN [_ k / n ]_ A e. dom vol -> U_ k e. NN ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) = U. { y | E. k e. NN y = ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) } )
16 11 15 syl5eq 
 |-  ( A. k e. NN [_ k / n ]_ A e. dom vol -> U_ n e. NN A = U. { y | E. k e. NN y = ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) } )
17 6 16 sylbi 
 |-  ( A. n e. NN A e. dom vol -> U_ n e. NN A = U. { y | E. k e. NN y = ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) } )
18 eqid 
 |-  ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) = ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) )
19 18 rnmpt 
 |-  ran ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) = { y | E. k e. NN y = ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) }
20 19 unieqi 
 |-  U. ran ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) = U. { y | E. k e. NN y = ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) }
21 17 20 eqtr4di 
 |-  ( A. n e. NN A e. dom vol -> U_ n e. NN A = U. ran ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) )
22 3 5 rspc 
 |-  ( k e. NN -> ( A. n e. NN A e. dom vol -> [_ k / n ]_ A e. dom vol ) )
23 22 impcom 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> [_ k / n ]_ A e. dom vol )
24 fzofi 
 |-  ( 1 ..^ k ) e. Fin
25 nfv 
 |-  F/ m A e. dom vol
26 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
27 26 nfel1 
 |-  F/ n [_ m / n ]_ A e. dom vol
28 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
29 28 eleq1d 
 |-  ( n = m -> ( A e. dom vol <-> [_ m / n ]_ A e. dom vol ) )
30 25 27 29 cbvralw 
 |-  ( A. n e. NN A e. dom vol <-> A. m e. NN [_ m / n ]_ A e. dom vol )
31 fzossnn 
 |-  ( 1 ..^ k ) C_ NN
32 ssralv 
 |-  ( ( 1 ..^ k ) C_ NN -> ( A. m e. NN [_ m / n ]_ A e. dom vol -> A. m e. ( 1 ..^ k ) [_ m / n ]_ A e. dom vol ) )
33 31 32 ax-mp 
 |-  ( A. m e. NN [_ m / n ]_ A e. dom vol -> A. m e. ( 1 ..^ k ) [_ m / n ]_ A e. dom vol )
34 30 33 sylbi 
 |-  ( A. n e. NN A e. dom vol -> A. m e. ( 1 ..^ k ) [_ m / n ]_ A e. dom vol )
35 34 adantr 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> A. m e. ( 1 ..^ k ) [_ m / n ]_ A e. dom vol )
36 finiunmbl 
 |-  ( ( ( 1 ..^ k ) e. Fin /\ A. m e. ( 1 ..^ k ) [_ m / n ]_ A e. dom vol ) -> U_ m e. ( 1 ..^ k ) [_ m / n ]_ A e. dom vol )
37 24 35 36 sylancr 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> U_ m e. ( 1 ..^ k ) [_ m / n ]_ A e. dom vol )
38 difmbl 
 |-  ( ( [_ k / n ]_ A e. dom vol /\ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A e. dom vol ) -> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) e. dom vol )
39 23 37 38 syl2anc 
 |-  ( ( A. n e. NN A e. dom vol /\ k e. NN ) -> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) e. dom vol )
40 39 fmpttd 
 |-  ( A. n e. NN A e. dom vol -> ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) : NN --> dom vol )
41 csbeq1 
 |-  ( i = m -> [_ i / n ]_ A = [_ m / n ]_ A )
42 41 iundisj2 
 |-  Disj_ i e. NN ( [_ i / n ]_ A \ U_ m e. ( 1 ..^ i ) [_ m / n ]_ A )
43 csbeq1 
 |-  ( k = i -> [_ k / n ]_ A = [_ i / n ]_ A )
44 oveq2 
 |-  ( k = i -> ( 1 ..^ k ) = ( 1 ..^ i ) )
45 44 iuneq1d 
 |-  ( k = i -> U_ m e. ( 1 ..^ k ) [_ m / n ]_ A = U_ m e. ( 1 ..^ i ) [_ m / n ]_ A )
46 43 45 difeq12d 
 |-  ( k = i -> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) = ( [_ i / n ]_ A \ U_ m e. ( 1 ..^ i ) [_ m / n ]_ A ) )
47 simpr 
 |-  ( ( A. n e. NN A e. dom vol /\ i e. NN ) -> i e. NN )
48 nfcsb1v 
 |-  F/_ n [_ i / n ]_ A
49 48 nfel1 
 |-  F/ n [_ i / n ]_ A e. dom vol
50 csbeq1a 
 |-  ( n = i -> A = [_ i / n ]_ A )
51 50 eleq1d 
 |-  ( n = i -> ( A e. dom vol <-> [_ i / n ]_ A e. dom vol ) )
52 49 51 rspc 
 |-  ( i e. NN -> ( A. n e. NN A e. dom vol -> [_ i / n ]_ A e. dom vol ) )
53 52 impcom 
 |-  ( ( A. n e. NN A e. dom vol /\ i e. NN ) -> [_ i / n ]_ A e. dom vol )
54 difexg 
 |-  ( [_ i / n ]_ A e. dom vol -> ( [_ i / n ]_ A \ U_ m e. ( 1 ..^ i ) [_ m / n ]_ A ) e. _V )
55 53 54 syl 
 |-  ( ( A. n e. NN A e. dom vol /\ i e. NN ) -> ( [_ i / n ]_ A \ U_ m e. ( 1 ..^ i ) [_ m / n ]_ A ) e. _V )
56 18 46 47 55 fvmptd3 
 |-  ( ( A. n e. NN A e. dom vol /\ i e. NN ) -> ( ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) ` i ) = ( [_ i / n ]_ A \ U_ m e. ( 1 ..^ i ) [_ m / n ]_ A ) )
57 56 disjeq2dv 
 |-  ( A. n e. NN A e. dom vol -> ( Disj_ i e. NN ( ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) ` i ) <-> Disj_ i e. NN ( [_ i / n ]_ A \ U_ m e. ( 1 ..^ i ) [_ m / n ]_ A ) ) )
58 42 57 mpbiri 
 |-  ( A. n e. NN A e. dom vol -> Disj_ i e. NN ( ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) ` i ) )
59 eqid 
 |-  ( y e. NN |-> ( vol* ` ( x i^i ( ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) ` y ) ) ) ) = ( y e. NN |-> ( vol* ` ( x i^i ( ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) ` y ) ) ) )
60 40 58 59 voliunlem2 
 |-  ( A. n e. NN A e. dom vol -> U. ran ( k e. NN |-> ( [_ k / n ]_ A \ U_ m e. ( 1 ..^ k ) [_ m / n ]_ A ) ) e. dom vol )
61 21 60 eqeltrd 
 |-  ( A. n e. NN A e. dom vol -> U_ n e. NN A e. dom vol )