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 n A dom vol n A dom vol

Proof

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