Metamath Proof Explorer

Theorem volfiniune

Description: The Lebesgue measure function is countably additive. This theorem is to volfiniun what voliune is to voliun . (Contributed by Thierry Arnoux, 16-Oct-2017)

Ref Expression
Assertion volfiniune 
|- ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) -> ( vol ` U_ n e. A B ) = sum* n e. A ( vol ` B ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) -> A e. Fin )
2 simpl2 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) -> A. n e. A B e. dom vol )
3 simpr 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) -> A. n e. A ( vol ` B ) e. RR )
4 r19.26 
 |-  ( A. n e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) <-> ( A. n e. A B e. dom vol /\ A. n e. A ( vol ` B ) e. RR ) )
5 2 3 4 sylanbrc 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) -> A. n e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) )
6 simpl3 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) -> Disj_ n e. A B )
7 volfiniun 
 |-  ( ( A e. Fin /\ A. n e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ n e. A B ) -> ( vol ` U_ n e. A B ) = sum_ n e. A ( vol ` B ) )
8 1 5 6 7 syl3anc 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) -> ( vol ` U_ n e. A B ) = sum_ n e. A ( vol ` B ) )
9 nfcv 
 |-  F/_ n A
10 9 nfel1 
 |-  F/ n A e. Fin
11 nfra1 
 |-  F/ n A. n e. A B e. dom vol
12 nfdisj1 
 |-  F/ n Disj_ n e. A B
13 10 11 12 nf3an 
 |-  F/ n ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B )
14 nfra1 
 |-  F/ n A. n e. A ( vol ` B ) e. RR
15 13 14 nfan 
 |-  F/ n ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR )
16 3 r19.21bi 
 |-  ( ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) /\ n e. A ) -> ( vol ` B ) e. RR )
17 rspa 
 |-  ( ( A. n e. A B e. dom vol /\ n e. A ) -> B e. dom vol )
18 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
19 18 ffvelcdmi 
 |-  ( B e. dom vol -> ( vol ` B ) e. ( 0 [,] +oo ) )
20 17 19 syl 
 |-  ( ( A. n e. A B e. dom vol /\ n e. A ) -> ( vol ` B ) e. ( 0 [,] +oo ) )
21 2 20 sylan 
 |-  ( ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) /\ n e. A ) -> ( vol ` B ) e. ( 0 [,] +oo ) )
22 0xr 
 |-  0 e. RR*
23 pnfxr 
 |-  +oo e. RR*
24 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( ( vol ` B ) e. ( 0 [,] +oo ) <-> ( ( vol ` B ) e. RR* /\ 0 <_ ( vol ` B ) /\ ( vol ` B ) <_ +oo ) ) )
25 22 23 24 mp2an 
 |-  ( ( vol ` B ) e. ( 0 [,] +oo ) <-> ( ( vol ` B ) e. RR* /\ 0 <_ ( vol ` B ) /\ ( vol ` B ) <_ +oo ) )
26 25 simp2bi 
 |-  ( ( vol ` B ) e. ( 0 [,] +oo ) -> 0 <_ ( vol ` B ) )
27 21 26 syl 
 |-  ( ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) /\ n e. A ) -> 0 <_ ( vol ` B ) )
28 ltpnf 
 |-  ( ( vol ` B ) e. RR -> ( vol ` B ) < +oo )
29 16 28 syl 
 |-  ( ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) /\ n e. A ) -> ( vol ` B ) < +oo )
30 0re 
 |-  0 e. RR
31 elico2 
 |-  ( ( 0 e. RR /\ +oo e. RR* ) -> ( ( vol ` B ) e. ( 0 [,) +oo ) <-> ( ( vol ` B ) e. RR /\ 0 <_ ( vol ` B ) /\ ( vol ` B ) < +oo ) ) )
32 30 23 31 mp2an 
 |-  ( ( vol ` B ) e. ( 0 [,) +oo ) <-> ( ( vol ` B ) e. RR /\ 0 <_ ( vol ` B ) /\ ( vol ` B ) < +oo ) )
33 16 27 29 32 syl3anbrc 
 |-  ( ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) /\ n e. A ) -> ( vol ` B ) e. ( 0 [,) +oo ) )
34 9 15 1 33 esumpfinvalf 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) -> sum* n e. A ( vol ` B ) = sum_ n e. A ( vol ` B ) )
35 8 34 eqtr4d 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ A. n e. A ( vol ` B ) e. RR ) -> ( vol ` U_ n e. A B ) = sum* n e. A ( vol ` B ) )
36 simpr 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> E. n e. A ( vol ` B ) = +oo )
37 nfv 
 |-  F/ k ( vol ` B ) = +oo
38 nfcv 
 |-  F/_ n vol
39 nfcsb1v 
 |-  F/_ n [_ k / n ]_ B
40 38 39 nffv 
 |-  F/_ n ( vol ` [_ k / n ]_ B )
41 40 nfeq1 
 |-  F/ n ( vol ` [_ k / n ]_ B ) = +oo
42 csbeq1a 
 |-  ( n = k -> B = [_ k / n ]_ B )
43 42 fveqeq2d 
 |-  ( n = k -> ( ( vol ` B ) = +oo <-> ( vol ` [_ k / n ]_ B ) = +oo ) )
44 37 41 43 cbvrexw 
 |-  ( E. n e. A ( vol ` B ) = +oo <-> E. k e. A ( vol ` [_ k / n ]_ B ) = +oo )
45 36 44 sylib 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> E. k e. A ( vol ` [_ k / n ]_ B ) = +oo )
46 39 nfel1 
 |-  F/ n [_ k / n ]_ B e. dom vol
47 42 eleq1d 
 |-  ( n = k -> ( B e. dom vol <-> [_ k / n ]_ B e. dom vol ) )
48 46 47 rspc 
 |-  ( k e. A -> ( A. n e. A B e. dom vol -> [_ k / n ]_ B e. dom vol ) )
49 48 impcom 
 |-  ( ( A. n e. A B e. dom vol /\ k e. A ) -> [_ k / n ]_ B e. dom vol )
50 49 adantll 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol ) /\ k e. A ) -> [_ k / n ]_ B e. dom vol )
51 finiunmbl 
 |-  ( ( A e. Fin /\ A. n e. A B e. dom vol ) -> U_ n e. A B e. dom vol )
52 51 adantr 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol ) /\ k e. A ) -> U_ n e. A B e. dom vol )
53 nfcv 
 |-  F/_ n k
54 9 53 39 42 ssiun2sf 
 |-  ( k e. A -> [_ k / n ]_ B C_ U_ n e. A B )
55 54 adantl 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol ) /\ k e. A ) -> [_ k / n ]_ B C_ U_ n e. A B )
56 volss 
 |-  ( ( [_ k / n ]_ B e. dom vol /\ U_ n e. A B e. dom vol /\ [_ k / n ]_ B C_ U_ n e. A B ) -> ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) )
57 50 52 55 56 syl3anc 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol ) /\ k e. A ) -> ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) )
58 57 3adantl3 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ k e. A ) -> ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) )
59 58 adantlr 
 |-  ( ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) /\ k e. A ) -> ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) )
60 59 ralrimiva 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> A. k e. A ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) )
61 r19.29r 
 |-  ( ( E. k e. A ( vol ` [_ k / n ]_ B ) = +oo /\ A. k e. A ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) ) -> E. k e. A ( ( vol ` [_ k / n ]_ B ) = +oo /\ ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) ) )
62 45 60 61 syl2anc 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> E. k e. A ( ( vol ` [_ k / n ]_ B ) = +oo /\ ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) ) )
63 breq1 
 |-  ( ( vol ` [_ k / n ]_ B ) = +oo -> ( ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) <-> +oo <_ ( vol ` U_ n e. A B ) ) )
64 63 biimpa 
 |-  ( ( ( vol ` [_ k / n ]_ B ) = +oo /\ ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) ) -> +oo <_ ( vol ` U_ n e. A B ) )
65 64 reximi 
 |-  ( E. k e. A ( ( vol ` [_ k / n ]_ B ) = +oo /\ ( vol ` [_ k / n ]_ B ) <_ ( vol ` U_ n e. A B ) ) -> E. k e. A +oo <_ ( vol ` U_ n e. A B ) )
66 62 65 syl 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> E. k e. A +oo <_ ( vol ` U_ n e. A B ) )
67 rexex 
 |-  ( E. k e. A +oo <_ ( vol ` U_ n e. A B ) -> E. k +oo <_ ( vol ` U_ n e. A B ) )
68 19.9v 
 |-  ( E. k +oo <_ ( vol ` U_ n e. A B ) <-> +oo <_ ( vol ` U_ n e. A B ) )
69 67 68 sylib 
 |-  ( E. k e. A +oo <_ ( vol ` U_ n e. A B ) -> +oo <_ ( vol ` U_ n e. A B ) )
70 66 69 syl 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> +oo <_ ( vol ` U_ n e. A B ) )
71 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
72 18 ffvelcdmi 
 |-  ( U_ n e. A B e. dom vol -> ( vol ` U_ n e. A B ) e. ( 0 [,] +oo ) )
73 71 72 sselid 
 |-  ( U_ n e. A B e. dom vol -> ( vol ` U_ n e. A B ) e. RR* )
74 51 73 syl 
 |-  ( ( A e. Fin /\ A. n e. A B e. dom vol ) -> ( vol ` U_ n e. A B ) e. RR* )
75 74 3adant3 
 |-  ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) -> ( vol ` U_ n e. A B ) e. RR* )
76 75 adantr 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> ( vol ` U_ n e. A B ) e. RR* )
77 xgepnf 
 |-  ( ( vol ` U_ n e. A B ) e. RR* -> ( +oo <_ ( vol ` U_ n e. A B ) <-> ( vol ` U_ n e. A B ) = +oo ) )
78 76 77 syl 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> ( +oo <_ ( vol ` U_ n e. A B ) <-> ( vol ` U_ n e. A B ) = +oo ) )
79 70 78 mpbid 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> ( vol ` U_ n e. A B ) = +oo )
80 nfre1 
 |-  F/ n E. n e. A ( vol ` B ) = +oo
81 13 80 nfan 
 |-  F/ n ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo )
82 simpl1 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> A e. Fin )
83 20 3ad2antl2 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ n e. A ) -> ( vol ` B ) e. ( 0 [,] +oo ) )
84 83 adantlr 
 |-  ( ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) /\ n e. A ) -> ( vol ` B ) e. ( 0 [,] +oo ) )
85 81 82 84 36 esumpinfval 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> sum* n e. A ( vol ` B ) = +oo )
86 79 85 eqtr4d 
 |-  ( ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) /\ E. n e. A ( vol ` B ) = +oo ) -> ( vol ` U_ n e. A B ) = sum* n e. A ( vol ` B ) )
87 exmid 
 |-  ( A. n e. A ( vol ` B ) e. RR \/ -. A. n e. A ( vol ` B ) e. RR )
88 rexnal 
 |-  ( E. n e. A -. ( vol ` B ) e. RR <-> -. A. n e. A ( vol ` B ) e. RR )
89 88 orbi2i 
 |-  ( ( A. n e. A ( vol ` B ) e. RR \/ E. n e. A -. ( vol ` B ) e. RR ) <-> ( A. n e. A ( vol ` B ) e. RR \/ -. A. n e. A ( vol ` B ) e. RR ) )
90 87 89 mpbir 
 |-  ( A. n e. A ( vol ` B ) e. RR \/ E. n e. A -. ( vol ` B ) e. RR )
91 r19.29 
 |-  ( ( A. n e. A B e. dom vol /\ E. n e. A -. ( vol ` B ) e. RR ) -> E. n e. A ( B e. dom vol /\ -. ( vol ` B ) e. RR ) )
92 xrge0nre 
 |-  ( ( ( vol ` B ) e. ( 0 [,] +oo ) /\ -. ( vol ` B ) e. RR ) -> ( vol ` B ) = +oo )
93 19 92 sylan 
 |-  ( ( B e. dom vol /\ -. ( vol ` B ) e. RR ) -> ( vol ` B ) = +oo )
94 93 reximi 
 |-  ( E. n e. A ( B e. dom vol /\ -. ( vol ` B ) e. RR ) -> E. n e. A ( vol ` B ) = +oo )
95 91 94 syl 
 |-  ( ( A. n e. A B e. dom vol /\ E. n e. A -. ( vol ` B ) e. RR ) -> E. n e. A ( vol ` B ) = +oo )
96 95 ex 
 |-  ( A. n e. A B e. dom vol -> ( E. n e. A -. ( vol ` B ) e. RR -> E. n e. A ( vol ` B ) = +oo ) )
97 96 orim2d 
 |-  ( A. n e. A B e. dom vol -> ( ( A. n e. A ( vol ` B ) e. RR \/ E. n e. A -. ( vol ` B ) e. RR ) -> ( A. n e. A ( vol ` B ) e. RR \/ E. n e. A ( vol ` B ) = +oo ) ) )
98 90 97 mpi 
 |-  ( A. n e. A B e. dom vol -> ( A. n e. A ( vol ` B ) e. RR \/ E. n e. A ( vol ` B ) = +oo ) )
99 98 3ad2ant2 
 |-  ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) -> ( A. n e. A ( vol ` B ) e. RR \/ E. n e. A ( vol ` B ) = +oo ) )
100 35 86 99 mpjaodan 
 |-  ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj_ n e. A B ) -> ( vol ` U_ n e. A B ) = sum* n e. A ( vol ` B ) )