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 syl5eq 
 |-  ( ( 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* , < ) )