Metamath Proof Explorer


Theorem voliun

Description: The Lebesgue measure function is countably additive. (Contributed by Mario Carneiro, 18-Mar-2014) (Proof shortened by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypotheses voliun.1 S = seq 1 + G
voliun.2 G = n vol A
Assertion voliun n A dom vol vol A Disj n A vol n A = sup ran S * <

Proof

Step Hyp Ref Expression
1 voliun.1 S = seq 1 + G
2 voliun.2 G = n vol A
3 simpl A dom vol vol A A dom vol
4 3 ralimi n A dom vol vol A n A dom vol
5 4 adantr n A dom vol vol A Disj n A n A dom vol
6 eqid n A = n A
7 6 fmpt n A dom vol n A : dom vol
8 5 7 sylib n A dom vol vol A Disj n A n A : dom vol
9 6 fvmpt2 n A dom vol n A n = A
10 9 adantrr n A dom vol vol A n A n = A
11 10 ralimiaa n A dom vol vol A n n A n = A
12 disjeq2 n n A n = A Disj n n A n Disj n A
13 11 12 syl n A dom vol vol A Disj n n A n Disj n A
14 13 biimpar n A dom vol vol A Disj n A Disj n n A n
15 nfcv _ i n A n
16 nffvmpt1 _ n n A i
17 fveq2 n = i n A n = n A i
18 15 16 17 cbvdisj Disj n n A n Disj i n A i
19 14 18 sylib n A dom vol vol A Disj n A Disj i n A i
20 eqid m vol * x n A m = m vol * x n A m
21 eqid seq 1 + n vol n A n = seq 1 + n vol n A n
22 nfcv _ m vol n A n
23 nfcv _ n vol
24 nffvmpt1 _ n n A m
25 23 24 nffv _ n vol n A m
26 2fveq3 n = m vol n A n = vol n A m
27 22 25 26 cbvmpt n vol n A n = m vol n A m
28 9 fveq2d n A dom vol vol n A n = vol A
29 28 eleq1d n A dom vol vol n A n vol A
30 29 biimprd n A dom vol vol A vol n A n
31 30 impr n A dom vol vol A vol n A n
32 31 ralimiaa n A dom vol vol A n vol n A n
33 32 adantr n A dom vol vol A Disj n A n vol n A n
34 nfv i vol n A n
35 23 16 nffv _ n vol n A i
36 35 nfel1 n vol n A i
37 2fveq3 n = i vol n A n = vol n A i
38 37 eleq1d n = i vol n A n vol n A i
39 34 36 38 cbvralw n vol n A n i vol n A i
40 33 39 sylib n A dom vol vol A Disj n A i vol n A i
41 8 19 20 21 27 40 voliunlem3 n A dom vol vol A Disj n A vol ran n A = sup ran seq 1 + n vol n A n * <
42 dfiun2g n A dom vol n A = x | n x = A
43 5 42 syl n A dom vol vol A Disj n A n A = x | n x = A
44 6 rnmpt ran n A = x | n x = A
45 44 unieqi ran n A = x | n x = A
46 43 45 syl6eqr n A dom vol vol A Disj n A n A = ran n A
47 46 fveq2d n A dom vol vol A Disj n A vol n A = vol ran n A
48 eqid =
49 28 adantrr n A dom vol vol A vol n A n = vol A
50 49 ralimiaa n A dom vol vol A n vol n A n = vol A
51 50 adantr n A dom vol vol A Disj n A n vol n A n = vol A
52 mpteq12 = n vol n A n = vol A n vol n A n = n vol A
53 48 51 52 sylancr n A dom vol vol A Disj n A n vol n A n = n vol A
54 53 2 syl6reqr n A dom vol vol A Disj n A G = n vol n A n
55 54 seqeq3d n A dom vol vol A Disj n A seq 1 + G = seq 1 + n vol n A n
56 1 55 syl5eq n A dom vol vol A Disj n A S = seq 1 + n vol n A n
57 56 rneqd n A dom vol vol A Disj n A ran S = ran seq 1 + n vol n A n
58 57 supeq1d n A dom vol vol A Disj n A sup ran S * < = sup ran seq 1 + n vol n A n * <
59 41 47 58 3eqtr4d n A dom vol vol A Disj n A vol n A = sup ran S * <