Metamath Proof Explorer

Theorem meaiuninc3

Description: Measures are continuous from below: 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 the general case of Proposition 112C (e) of Fremlin1 p. 16 . This theorem generalizes meaiuninc and meaiuninc2 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 meaiuninc3.p 
 |-  F/ n ph
2 meaiuninc3.f 
 |-  F/_ n E
3 meaiuninc3.m 
 |-  ( ph -> M e. Meas )
4 meaiuninc3.n 
 |-  ( ph -> N e. ZZ )
5 meaiuninc3.z 
 |-  Z = ( ZZ>= ` N )
6 meaiuninc3.e 
 |-  ( ph -> E : Z --> dom M )
7 meaiuninc3.i 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) )
8 meaiuninc3.s 
 |-  S = ( n e. Z |-> ( M ` ( E ` n ) ) )
9 nfv 
 |-  F/ n k e. Z
10 1 9 nfan 
 |-  F/ n ( ph /\ k e. Z )
11 nfcv 
 |-  F/_ n k
12 2 11 nffv 
 |-  F/_ n ( E ` k )
13 nfcv 
 |-  F/_ n ( k + 1 )
14 2 13 nffv 
 |-  F/_ n ( E ` ( k + 1 ) )
15 12 14 nfss 
 |-  F/ n ( E ` k ) C_ ( E ` ( k + 1 ) )
16 10 15 nfim 
 |-  F/ n ( ( ph /\ k e. Z ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) )
17 eleq1w 
 |-  ( n = k -> ( n e. Z <-> k e. Z ) )
18 17 anbi2d 
 |-  ( n = k -> ( ( ph /\ n e. Z ) <-> ( ph /\ k e. Z ) ) )
19 fveq2 
 |-  ( n = k -> ( E ` n ) = ( E ` k ) )
20 fvoveq1 
 |-  ( n = k -> ( E ` ( n + 1 ) ) = ( E ` ( k + 1 ) ) )
21 19 20 sseq12d 
 |-  ( n = k -> ( ( E ` n ) C_ ( E ` ( n + 1 ) ) <-> ( E ` k ) C_ ( E ` ( k + 1 ) ) ) )
22 18 21 imbi12d 
 |-  ( n = k -> ( ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) ) <-> ( ( ph /\ k e. Z ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) ) ) )
23 16 22 7 chvarfv 
 |-  ( ( ph /\ k e. Z ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) )
24 nfcv 
 |-  F/_ k M
25 nfcv 
 |-  F/_ k ( E ` n )
26 24 25 nffv 
 |-  F/_ k ( M ` ( E ` n ) )
27 nfcv 
 |-  F/_ n M
28 27 12 nffv 
 |-  F/_ n ( M ` ( E ` k ) )
29 2fveq3 
 |-  ( n = k -> ( M ` ( E ` n ) ) = ( M ` ( E ` k ) ) )
30 26 28 29 cbvmpt 
 |-  ( n e. Z |-> ( M ` ( E ` n ) ) ) = ( k e. Z |-> ( M ` ( E ` k ) ) )
31 8 30 eqtri 
 |-  S = ( k e. Z |-> ( M ` ( E ` k ) ) )
32 3 4 5 6 23 31 meaiuninc3v 
 |-  ( ph -> S ~~>* ( M ` U_ k e. Z ( E ` k ) ) )
33 fveq2 
 |-  ( k = n -> ( E ` k ) = ( E ` n ) )
34 12 25 33 cbviun 
 |-  U_ k e. Z ( E ` k ) = U_ n e. Z ( E ` n )
35 34 fveq2i 
 |-  ( M ` U_ k e. Z ( E ` k ) ) = ( M ` U_ n e. Z ( E ` n ) )
36 32 35 breqtrdi 
 |-  ( ph -> S ~~>* ( M ` U_ n e. Z ( E ` n ) ) )