Metamath Proof Explorer

Theorem voliunsge0lem

Description: The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses voliunsge0lem.s 
|- S = seq 1 ( + , G )
voliunsge0lem.g 
|- G = ( n e. NN |-> ( vol ` ( E ` n ) ) )
voliunsge0lem.e 
|- ( ph -> E : NN --> dom vol )
voliunsge0lem.d 
|- ( ph -> Disj_ n e. NN ( E ` n ) )
Assertion voliunsge0lem 
|- ( ph -> ( vol ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 voliunsge0lem.s 
 |-  S = seq 1 ( + , G )
2 voliunsge0lem.g 
 |-  G = ( n e. NN |-> ( vol ` ( E ` n ) ) )
3 voliunsge0lem.e 
 |-  ( ph -> E : NN --> dom vol )
4 voliunsge0lem.d 
 |-  ( ph -> Disj_ n e. NN ( E ` n ) )
5 nfv 
 |-  F/ n ph
6 nfcv 
 |-  F/_ n vol
7 nfiu1 
 |-  F/_ n U_ n e. NN ( E ` n )
8 6 7 nffv 
 |-  F/_ n ( vol ` U_ n e. NN ( E ` n ) )
9 8 nfeq1 
 |-  F/ n ( vol ` U_ n e. NN ( E ` n ) ) = +oo
10 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
11 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
12 11 a1i 
 |-  ( ph -> vol : dom vol --> ( 0 [,] +oo ) )
13 3 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) e. dom vol )
14 13 ralrimiva 
 |-  ( ph -> A. n e. NN ( E ` n ) e. dom vol )
15 iunmbl 
 |-  ( A. n e. NN ( E ` n ) e. dom vol -> U_ n e. NN ( E ` n ) e. dom vol )
16 14 15 syl 
 |-  ( ph -> U_ n e. NN ( E ` n ) e. dom vol )
17 12 16 ffvelrnd 
 |-  ( ph -> ( vol ` U_ n e. NN ( E ` n ) ) e. ( 0 [,] +oo ) )
18 10 17 sseldi 
 |-  ( ph -> ( vol ` U_ n e. NN ( E ` n ) ) e. RR* )
19 18 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( vol ` U_ n e. NN ( E ` n ) ) e. RR* )
20 19 3adant3 
 |-  ( ( ph /\ n e. NN /\ ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` U_ n e. NN ( E ` n ) ) e. RR* )
21 id 
 |-  ( ( vol ` ( E ` n ) ) = +oo -> ( vol ` ( E ` n ) ) = +oo )
22 21 eqcomd 
 |-  ( ( vol ` ( E ` n ) ) = +oo -> +oo = ( vol ` ( E ` n ) ) )
23 22 3ad2ant3 
 |-  ( ( ph /\ n e. NN /\ ( vol ` ( E ` n ) ) = +oo ) -> +oo = ( vol ` ( E ` n ) ) )
24 16 adantr 
 |-  ( ( ph /\ n e. NN ) -> U_ n e. NN ( E ` n ) e. dom vol )
25 ssiun2 
 |-  ( n e. NN -> ( E ` n ) C_ U_ n e. NN ( E ` n ) )
26 25 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) C_ U_ n e. NN ( E ` n ) )
27 volss 
 |-  ( ( ( E ` n ) e. dom vol /\ U_ n e. NN ( E ` n ) e. dom vol /\ ( E ` n ) C_ U_ n e. NN ( E ` n ) ) -> ( vol ` ( E ` n ) ) <_ ( vol ` U_ n e. NN ( E ` n ) ) )
28 13 24 26 27 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( vol ` ( E ` n ) ) <_ ( vol ` U_ n e. NN ( E ` n ) ) )
29 28 3adant3 
 |-  ( ( ph /\ n e. NN /\ ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` ( E ` n ) ) <_ ( vol ` U_ n e. NN ( E ` n ) ) )
30 23 29 eqbrtrd 
 |-  ( ( ph /\ n e. NN /\ ( vol ` ( E ` n ) ) = +oo ) -> +oo <_ ( vol ` U_ n e. NN ( E ` n ) ) )
31 20 30 xrgepnfd 
 |-  ( ( ph /\ n e. NN /\ ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` U_ n e. NN ( E ` n ) ) = +oo )
32 31 3exp 
 |-  ( ph -> ( n e. NN -> ( ( vol ` ( E ` n ) ) = +oo -> ( vol ` U_ n e. NN ( E ` n ) ) = +oo ) ) )
33 5 9 32 rexlimd 
 |-  ( ph -> ( E. n e. NN ( vol ` ( E ` n ) ) = +oo -> ( vol ` U_ n e. NN ( E ` n ) ) = +oo ) )
34 33 imp 
 |-  ( ( ph /\ E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` U_ n e. NN ( E ` n ) ) = +oo )
35 nfre1 
 |-  F/ n E. n e. NN ( vol ` ( E ` n ) ) = +oo
36 5 35 nfan 
 |-  F/ n ( ph /\ E. n e. NN ( vol ` ( E ` n ) ) = +oo )
37 nnex 
 |-  NN e. _V
38 37 a1i 
 |-  ( ( ph /\ E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> NN e. _V )
39 11 a1i 
 |-  ( ( ph /\ n e. NN ) -> vol : dom vol --> ( 0 [,] +oo ) )
40 39 13 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( vol ` ( E ` n ) ) e. ( 0 [,] +oo ) )
41 40 adantlr 
 |-  ( ( ( ph /\ E. n e. NN ( vol ` ( E ` n ) ) = +oo ) /\ n e. NN ) -> ( vol ` ( E ` n ) ) e. ( 0 [,] +oo ) )
42 simpr 
 |-  ( ( ph /\ E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> E. n e. NN ( vol ` ( E ` n ) ) = +oo )
43 36 38 41 42 sge0pnfmpt 
 |-  ( ( ph /\ E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) = +oo )
44 34 43 eqtr4d 
 |-  ( ( ph /\ E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) )
45 ralnex 
 |-  ( A. n e. NN -. ( vol ` ( E ` n ) ) = +oo <-> -. E. n e. NN ( vol ` ( E ` n ) ) = +oo )
46 45 biimpri 
 |-  ( -. E. n e. NN ( vol ` ( E ` n ) ) = +oo -> A. n e. NN -. ( vol ` ( E ` n ) ) = +oo )
47 46 adantl 
 |-  ( ( ph /\ -. E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> A. n e. NN -. ( vol ` ( E ` n ) ) = +oo )
48 40 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ -. ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` ( E ` n ) ) e. ( 0 [,] +oo ) )
49 21 necon3bi 
 |-  ( -. ( vol ` ( E ` n ) ) = +oo -> ( vol ` ( E ` n ) ) =/= +oo )
50 49 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ -. ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` ( E ` n ) ) =/= +oo )
51 ge0xrre 
 |-  ( ( ( vol ` ( E ` n ) ) e. ( 0 [,] +oo ) /\ ( vol ` ( E ` n ) ) =/= +oo ) -> ( vol ` ( E ` n ) ) e. RR )
52 48 50 51 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ -. ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` ( E ` n ) ) e. RR )
53 52 ex 
 |-  ( ( ph /\ n e. NN ) -> ( -. ( vol ` ( E ` n ) ) = +oo -> ( vol ` ( E ` n ) ) e. RR ) )
54 renepnf 
 |-  ( ( vol ` ( E ` n ) ) e. RR -> ( vol ` ( E ` n ) ) =/= +oo )
55 54 neneqd 
 |-  ( ( vol ` ( E ` n ) ) e. RR -> -. ( vol ` ( E ` n ) ) = +oo )
56 55 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( ( vol ` ( E ` n ) ) e. RR -> -. ( vol ` ( E ` n ) ) = +oo ) )
57 53 56 impbid 
 |-  ( ( ph /\ n e. NN ) -> ( -. ( vol ` ( E ` n ) ) = +oo <-> ( vol ` ( E ` n ) ) e. RR ) )
58 57 ralbidva 
 |-  ( ph -> ( A. n e. NN -. ( vol ` ( E ` n ) ) = +oo <-> A. n e. NN ( vol ` ( E ` n ) ) e. RR ) )
59 58 adantr 
 |-  ( ( ph /\ -. E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> ( A. n e. NN -. ( vol ` ( E ` n ) ) = +oo <-> A. n e. NN ( vol ` ( E ` n ) ) e. RR ) )
60 47 59 mpbid 
 |-  ( ( ph /\ -. E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> A. n e. NN ( vol ` ( E ` n ) ) e. RR )
61 nfra1 
 |-  F/ n A. n e. NN ( vol ` ( E ` n ) ) e. RR
62 5 61 nfan 
 |-  F/ n ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR )
63 13 adantlr 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> ( E ` n ) e. dom vol )
64 rspa 
 |-  ( ( A. n e. NN ( vol ` ( E ` n ) ) e. RR /\ n e. NN ) -> ( vol ` ( E ` n ) ) e. RR )
65 64 adantll 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> ( vol ` ( E ` n ) ) e. RR )
66 63 65 jca 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> ( ( E ` n ) e. dom vol /\ ( vol ` ( E ` n ) ) e. RR ) )
67 66 ex 
 |-  ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) -> ( n e. NN -> ( ( E ` n ) e. dom vol /\ ( vol ` ( E ` n ) ) e. RR ) ) )
68 62 67 ralrimi 
 |-  ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) -> A. n e. NN ( ( E ` n ) e. dom vol /\ ( vol ` ( E ` n ) ) e. RR ) )
69 4 adantr 
 |-  ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) -> Disj_ n e. NN ( E ` n ) )
70 1 2 voliun 
 |-  ( ( A. n e. NN ( ( E ` n ) e. dom vol /\ ( vol ` ( E ` n ) ) e. RR ) /\ Disj_ n e. NN ( E ` n ) ) -> ( vol ` U_ n e. NN ( E ` n ) ) = sup ( ran S , RR* , < ) )
71 68 69 70 syl2anc 
 |-  ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) -> ( vol ` U_ n e. NN ( E ` n ) ) = sup ( ran S , RR* , < ) )
72 1zzd 
 |-  ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) -> 1 e. ZZ )
73 nnuz 
 |-  NN = ( ZZ>= ` 1 )
74 nfv 
 |-  F/ n m e. NN
75 62 74 nfan 
 |-  F/ n ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ m e. NN )
76 nfv 
 |-  F/ n ( vol ` ( E ` m ) ) e. ( 0 [,) +oo )
77 75 76 nfim 
 |-  F/ n ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ m e. NN ) -> ( vol ` ( E ` m ) ) e. ( 0 [,) +oo ) )
78 eleq1w 
 |-  ( n = m -> ( n e. NN <-> m e. NN ) )
79 78 anbi2d 
 |-  ( n = m -> ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) <-> ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ m e. NN ) ) )
80 2fveq3 
 |-  ( n = m -> ( vol ` ( E ` n ) ) = ( vol ` ( E ` m ) ) )
81 80 eleq1d 
 |-  ( n = m -> ( ( vol ` ( E ` n ) ) e. ( 0 [,) +oo ) <-> ( vol ` ( E ` m ) ) e. ( 0 [,) +oo ) ) )
82 79 81 imbi12d 
 |-  ( n = m -> ( ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> ( vol ` ( E ` n ) ) e. ( 0 [,) +oo ) ) <-> ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ m e. NN ) -> ( vol ` ( E ` m ) ) e. ( 0 [,) +oo ) ) ) )
83 0xr 
 |-  0 e. RR*
84 83 a1i 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> 0 e. RR* )
85 pnfxr 
 |-  +oo e. RR*
86 85 a1i 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> +oo e. RR* )
87 65 rexrd 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> ( vol ` ( E ` n ) ) e. RR* )
88 volge0 
 |-  ( ( E ` n ) e. dom vol -> 0 <_ ( vol ` ( E ` n ) ) )
89 13 88 syl 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( vol ` ( E ` n ) ) )
90 89 adantlr 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> 0 <_ ( vol ` ( E ` n ) ) )
91 65 ltpnfd 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> ( vol ` ( E ` n ) ) < +oo )
92 84 86 87 90 91 elicod 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ n e. NN ) -> ( vol ` ( E ` n ) ) e. ( 0 [,) +oo ) )
93 77 82 92 chvarfv 
 |-  ( ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) /\ m e. NN ) -> ( vol ` ( E ` m ) ) e. ( 0 [,) +oo ) )
94 80 cbvmptv 
 |-  ( n e. NN |-> ( vol ` ( E ` n ) ) ) = ( m e. NN |-> ( vol ` ( E ` m ) ) )
95 93 94 fmptd 
 |-  ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) -> ( n e. NN |-> ( vol ` ( E ` n ) ) ) : NN --> ( 0 [,) +oo ) )
96 seqeq3 
 |-  ( G = ( n e. NN |-> ( vol ` ( E ` n ) ) ) -> seq 1 ( + , G ) = seq 1 ( + , ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) )
97 2 96 ax-mp 
 |-  seq 1 ( + , G ) = seq 1 ( + , ( n e. NN |-> ( vol ` ( E ` n ) ) ) )
98 1 97 eqtri 
 |-  S = seq 1 ( + , ( n e. NN |-> ( vol ` ( E ` n ) ) ) )
99 72 73 95 98 sge0seq 
 |-  ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) -> ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) = sup ( ran S , RR* , < ) )
100 71 99 eqtr4d 
 |-  ( ( ph /\ A. n e. NN ( vol ` ( E ` n ) ) e. RR ) -> ( vol ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) )
101 60 100 syldan 
 |-  ( ( ph /\ -. E. n e. NN ( vol ` ( E ` n ) ) = +oo ) -> ( vol ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) )
102 44 101 pm2.61dan 
 |-  ( ph -> ( vol ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) )