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 e. NN |-> ( vol ` A ) )
Assertion voliun
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sup ( ran S , RR* , < ) )

Proof

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