Metamath Proof Explorer

Theorem meaiunlelem

Description: The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses meaiunlelem.1 
|- F/ n ph
meaiunlelem.m 
|- ( ph -> M e. Meas )
meaiunlelem.s 
|- S = dom M
meaiunlelem.z 
|- Z = ( ZZ>= ` N )
meaiunlelem.e 
|- ( ph -> E : Z --> S )
meaiunlelem.f 
|- F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
Assertion meaiunlelem 
|- ( ph -> ( M ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( M ` ( E ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 meaiunlelem.1 
 |-  F/ n ph
2 meaiunlelem.m 
 |-  ( ph -> M e. Meas )
3 meaiunlelem.s 
 |-  S = dom M
4 meaiunlelem.z 
 |-  Z = ( ZZ>= ` N )
5 meaiunlelem.e 
 |-  ( ph -> E : Z --> S )
6 meaiunlelem.f 
 |-  F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
7 1 4 5 6 iundjiun 
 |-  ( ph -> ( ( A. x e. Z U_ n e. ( N ... x ) ( F ` n ) = U_ n e. ( N ... x ) ( E ` n ) /\ U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) ) /\ Disj_ n e. Z ( F ` n ) ) )
8 7 simplrd 
 |-  ( ph -> U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) )
9 8 eqcomd 
 |-  ( ph -> U_ n e. Z ( E ` n ) = U_ n e. Z ( F ` n ) )
10 9 fveq2d 
 |-  ( ph -> ( M ` U_ n e. Z ( E ` n ) ) = ( M ` U_ n e. Z ( F ` n ) ) )
11 2 3 dmmeasal 
 |-  ( ph -> S e. SAlg )
12 11 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
13 5 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) e. S )
14 fzofi 
 |-  ( N ..^ n ) e. Fin
15 isfinite 
 |-  ( ( N ..^ n ) e. Fin <-> ( N ..^ n ) ~< _om )
16 15 biimpi 
 |-  ( ( N ..^ n ) e. Fin -> ( N ..^ n ) ~< _om )
17 sdomdom 
 |-  ( ( N ..^ n ) ~< _om -> ( N ..^ n ) ~<_ _om )
18 16 17 syl 
 |-  ( ( N ..^ n ) e. Fin -> ( N ..^ n ) ~<_ _om )
19 14 18 ax-mp 
 |-  ( N ..^ n ) ~<_ _om
20 19 a1i 
 |-  ( ph -> ( N ..^ n ) ~<_ _om )
21 5 adantr 
 |-  ( ( ph /\ i e. ( N ..^ n ) ) -> E : Z --> S )
22 elfzouz 
 |-  ( i e. ( N ..^ n ) -> i e. ( ZZ>= ` N ) )
23 4 eqcomi 
 |-  ( ZZ>= ` N ) = Z
24 22 23 eleqtrdi 
 |-  ( i e. ( N ..^ n ) -> i e. Z )
25 24 adantl 
 |-  ( ( ph /\ i e. ( N ..^ n ) ) -> i e. Z )
26 21 25 ffvelrnd 
 |-  ( ( ph /\ i e. ( N ..^ n ) ) -> ( E ` i ) e. S )
27 11 20 26 saliuncl 
 |-  ( ph -> U_ i e. ( N ..^ n ) ( E ` i ) e. S )
28 27 adantr 
 |-  ( ( ph /\ n e. Z ) -> U_ i e. ( N ..^ n ) ( E ` i ) e. S )
29 saldifcl2 
 |-  ( ( S e. SAlg /\ ( E ` n ) e. S /\ U_ i e. ( N ..^ n ) ( E ` i ) e. S ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. S )
30 12 13 28 29 syl3anc 
 |-  ( ( ph /\ n e. Z ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. S )
31 1 30 6 fmptdf 
 |-  ( ph -> F : Z --> S )
32 31 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. S )
33 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
34 33 uzct 
 |-  ( ZZ>= ` N ) ~<_ _om
35 4 34 eqbrtri 
 |-  Z ~<_ _om
36 35 a1i 
 |-  ( ph -> Z ~<_ _om )
37 7 simprd 
 |-  ( ph -> Disj_ n e. Z ( F ` n ) )
38 1 2 3 32 36 37 meadjiun 
 |-  ( ph -> ( M ` U_ n e. Z ( F ` n ) ) = ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) )
39 eqidd 
 |-  ( ph -> ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) = ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) )
40 10 38 39 3eqtrd 
 |-  ( ph -> ( M ` U_ n e. Z ( E ` n ) ) = ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) )
41 4 fvexi 
 |-  Z e. _V
42 41 a1i 
 |-  ( ph -> Z e. _V )
43 2 adantr 
 |-  ( ( ph /\ n e. Z ) -> M e. Meas )
44 43 3 32 meacl 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( F ` n ) ) e. ( 0 [,] +oo ) )
45 43 3 13 meacl 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) e. ( 0 [,] +oo ) )
46 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
47 difexg 
 |-  ( ( E ` n ) e. S -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V )
48 13 47 syl 
 |-  ( ( ph /\ n e. Z ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V )
49 6 fvmpt2 
 |-  ( ( n e. Z /\ ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V ) -> ( F ` n ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
50 46 48 49 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
51 difssd 
 |-  ( ( ph /\ n e. Z ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) C_ ( E ` n ) )
52 50 51 eqsstrd 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) C_ ( E ` n ) )
53 43 3 32 13 52 meassle 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( F ` n ) ) <_ ( M ` ( E ` n ) ) )
54 1 42 44 45 53 sge0lempt 
 |-  ( ph -> ( sum^ ` ( n e. Z |-> ( M ` ( F ` n ) ) ) ) <_ ( sum^ ` ( n e. Z |-> ( M ` ( E ` n ) ) ) ) )
55 40 54 eqbrtrd 
 |-  ( ph -> ( M ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( M ` ( E ` n ) ) ) ) )