Metamath Proof Explorer

Theorem meaiunincf

Description: Measures are continuous from below (bounded case): if E is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 13-Feb-2022)

Ref Expression
Hypotheses meaiunincf.p 
|- F/ n ph
meaiunincf.f 
|- F/_ n E
meaiunincf.m 
|- ( ph -> M e. Meas )
meaiunincf.n 
|- ( ph -> N e. ZZ )
meaiunincf.z 
|- Z = ( ZZ>= ` N )
meaiunincf.e 
|- ( ph -> E : Z --> dom M )
meaiunincf.i 
|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) )
meaiunincf.x 
|- ( ph -> E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
meaiunincf.s 
|- S = ( n e. Z |-> ( M ` ( E ` n ) ) )
Assertion meaiunincf 
|- ( ph -> S ~~> ( M ` U_ n e. Z ( E ` n ) ) )

Proof

Step Hyp Ref Expression
1 meaiunincf.p 
 |-  F/ n ph
2 meaiunincf.f 
 |-  F/_ n E
3 meaiunincf.m 
 |-  ( ph -> M e. Meas )
4 meaiunincf.n 
 |-  ( ph -> N e. ZZ )
5 meaiunincf.z 
 |-  Z = ( ZZ>= ` N )
6 meaiunincf.e 
 |-  ( ph -> E : Z --> dom M )
7 meaiunincf.i 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) )
8 meaiunincf.x 
 |-  ( ph -> E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
9 meaiunincf.s 
 |-  S = ( n e. Z |-> ( M ` ( E ` n ) ) )
10 nfv 
 |-  F/ n k e. Z
11 1 10 nfan 
 |-  F/ n ( ph /\ k e. Z )
12 nfcv 
 |-  F/_ n k
13 2 12 nffv 
 |-  F/_ n ( E ` k )
14 nfcv 
 |-  F/_ n ( k + 1 )
15 2 14 nffv 
 |-  F/_ n ( E ` ( k + 1 ) )
16 13 15 nfss 
 |-  F/ n ( E ` k ) C_ ( E ` ( k + 1 ) )
17 11 16 nfim 
 |-  F/ n ( ( ph /\ k e. Z ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) )
18 eleq1w 
 |-  ( n = k -> ( n e. Z <-> k e. Z ) )
19 18 anbi2d 
 |-  ( n = k -> ( ( ph /\ n e. Z ) <-> ( ph /\ k e. Z ) ) )
20 fveq2 
 |-  ( n = k -> ( E ` n ) = ( E ` k ) )
21 fvoveq1 
 |-  ( n = k -> ( E ` ( n + 1 ) ) = ( E ` ( k + 1 ) ) )
22 20 21 sseq12d 
 |-  ( n = k -> ( ( E ` n ) C_ ( E ` ( n + 1 ) ) <-> ( E ` k ) C_ ( E ` ( k + 1 ) ) ) )
23 19 22 imbi12d 
 |-  ( n = k -> ( ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) ) <-> ( ( ph /\ k e. Z ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) ) ) )
24 17 23 7 chvarfv 
 |-  ( ( ph /\ k e. Z ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) )
25 breq2 
 |-  ( x = y -> ( ( M ` ( E ` n ) ) <_ x <-> ( M ` ( E ` n ) ) <_ y ) )
26 25 ralbidv 
 |-  ( x = y -> ( A. n e. Z ( M ` ( E ` n ) ) <_ x <-> A. n e. Z ( M ` ( E ` n ) ) <_ y ) )
27 nfv 
 |-  F/ k ( M ` ( E ` n ) ) <_ y
28 nfcv 
 |-  F/_ n M
29 28 13 nffv 
 |-  F/_ n ( M ` ( E ` k ) )
30 nfcv 
 |-  F/_ n <_
31 nfcv 
 |-  F/_ n y
32 29 30 31 nfbr 
 |-  F/ n ( M ` ( E ` k ) ) <_ y
33 2fveq3 
 |-  ( n = k -> ( M ` ( E ` n ) ) = ( M ` ( E ` k ) ) )
34 33 breq1d 
 |-  ( n = k -> ( ( M ` ( E ` n ) ) <_ y <-> ( M ` ( E ` k ) ) <_ y ) )
35 27 32 34 cbvralw 
 |-  ( A. n e. Z ( M ` ( E ` n ) ) <_ y <-> A. k e. Z ( M ` ( E ` k ) ) <_ y )
36 35 a1i 
 |-  ( x = y -> ( A. n e. Z ( M ` ( E ` n ) ) <_ y <-> A. k e. Z ( M ` ( E ` k ) ) <_ y ) )
37 26 36 bitrd 
 |-  ( x = y -> ( A. n e. Z ( M ` ( E ` n ) ) <_ x <-> A. k e. Z ( M ` ( E ` k ) ) <_ y ) )
38 37 cbvrexvw 
 |-  ( E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x <-> E. y e. RR A. k e. Z ( M ` ( E ` k ) ) <_ y )
39 8 38 sylib 
 |-  ( ph -> E. y e. RR A. k e. Z ( M ` ( E ` k ) ) <_ y )
40 nfcv 
 |-  F/_ k ( M ` ( E ` n ) )
41 40 29 33 cbvmpt 
 |-  ( n e. Z |-> ( M ` ( E ` n ) ) ) = ( k e. Z |-> ( M ` ( E ` k ) ) )
42 9 41 eqtri 
 |-  S = ( k e. Z |-> ( M ` ( E ` k ) ) )
43 3 4 5 6 24 39 42 meaiuninc 
 |-  ( ph -> S ~~> ( M ` U_ k e. Z ( E ` k ) ) )
44 nfcv 
 |-  F/_ k ( E ` n )
45 fveq2 
 |-  ( k = n -> ( E ` k ) = ( E ` n ) )
46 13 44 45 cbviun 
 |-  U_ k e. Z ( E ` k ) = U_ n e. Z ( E ` n )
47 46 fveq2i 
 |-  ( M ` U_ k e. Z ( E ` k ) ) = ( M ` U_ n e. Z ( E ` n ) )
48 43 47 breqtrdi 
 |-  ( ph -> S ~~> ( M ` U_ n e. Z ( E ` n ) ) )