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 𝑛 𝜑
meaiunlelem.m ( 𝜑𝑀 ∈ Meas )
meaiunlelem.s 𝑆 = dom 𝑀
meaiunlelem.z 𝑍 = ( ℤ𝑁 )
meaiunlelem.e ( 𝜑𝐸 : 𝑍𝑆 )
meaiunlelem.f 𝐹 = ( 𝑛𝑍 ↦ ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) )
Assertion meaiunlelem ( 𝜑 → ( 𝑀 𝑛𝑍 ( 𝐸𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛𝑍 ↦ ( 𝑀 ‘ ( 𝐸𝑛 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 meaiunlelem.1 𝑛 𝜑
2 meaiunlelem.m ( 𝜑𝑀 ∈ Meas )
3 meaiunlelem.s 𝑆 = dom 𝑀
4 meaiunlelem.z 𝑍 = ( ℤ𝑁 )
5 meaiunlelem.e ( 𝜑𝐸 : 𝑍𝑆 )
6 meaiunlelem.f 𝐹 = ( 𝑛𝑍 ↦ ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) )
7 1 4 5 6 iundjiun ( 𝜑 → ( ( ∀ 𝑥𝑍 𝑛 ∈ ( 𝑁 ... 𝑥 ) ( 𝐹𝑛 ) = 𝑛 ∈ ( 𝑁 ... 𝑥 ) ( 𝐸𝑛 ) ∧ 𝑛𝑍 ( 𝐹𝑛 ) = 𝑛𝑍 ( 𝐸𝑛 ) ) ∧ Disj 𝑛𝑍 ( 𝐹𝑛 ) ) )
8 7 simplrd ( 𝜑 𝑛𝑍 ( 𝐹𝑛 ) = 𝑛𝑍 ( 𝐸𝑛 ) )
9 8 eqcomd ( 𝜑 𝑛𝑍 ( 𝐸𝑛 ) = 𝑛𝑍 ( 𝐹𝑛 ) )
10 9 fveq2d ( 𝜑 → ( 𝑀 𝑛𝑍 ( 𝐸𝑛 ) ) = ( 𝑀 𝑛𝑍 ( 𝐹𝑛 ) ) )
11 2 3 dmmeasal ( 𝜑𝑆 ∈ SAlg )
12 11 adantr ( ( 𝜑𝑛𝑍 ) → 𝑆 ∈ SAlg )
13 5 ffvelrnda ( ( 𝜑𝑛𝑍 ) → ( 𝐸𝑛 ) ∈ 𝑆 )
14 fzofi ( 𝑁 ..^ 𝑛 ) ∈ Fin
15 isfinite ( ( 𝑁 ..^ 𝑛 ) ∈ Fin ↔ ( 𝑁 ..^ 𝑛 ) ≺ ω )
16 15 biimpi ( ( 𝑁 ..^ 𝑛 ) ∈ Fin → ( 𝑁 ..^ 𝑛 ) ≺ ω )
17 sdomdom ( ( 𝑁 ..^ 𝑛 ) ≺ ω → ( 𝑁 ..^ 𝑛 ) ≼ ω )
18 16 17 syl ( ( 𝑁 ..^ 𝑛 ) ∈ Fin → ( 𝑁 ..^ 𝑛 ) ≼ ω )
19 14 18 ax-mp ( 𝑁 ..^ 𝑛 ) ≼ ω
20 19 a1i ( 𝜑 → ( 𝑁 ..^ 𝑛 ) ≼ ω )
21 5 adantr ( ( 𝜑𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝐸 : 𝑍𝑆 )
22 elfzouz ( 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) → 𝑖 ∈ ( ℤ𝑁 ) )
23 4 eqcomi ( ℤ𝑁 ) = 𝑍
24 22 23 eleqtrdi ( 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) → 𝑖𝑍 )
25 24 adantl ( ( 𝜑𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖𝑍 )
26 21 25 ffvelrnd ( ( 𝜑𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝐸𝑖 ) ∈ 𝑆 )
27 11 20 26 saliuncl ( 𝜑 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ∈ 𝑆 )
28 27 adantr ( ( 𝜑𝑛𝑍 ) → 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ∈ 𝑆 )
29 saldifcl2 ( ( 𝑆 ∈ SAlg ∧ ( 𝐸𝑛 ) ∈ 𝑆 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ∈ 𝑆 ) → ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) ∈ 𝑆 )
30 12 13 28 29 syl3anc ( ( 𝜑𝑛𝑍 ) → ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) ∈ 𝑆 )
31 1 30 6 fmptdf ( 𝜑𝐹 : 𝑍𝑆 )
32 31 ffvelrnda ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) ∈ 𝑆 )
33 eqid ( ℤ𝑁 ) = ( ℤ𝑁 )
34 33 uzct ( ℤ𝑁 ) ≼ ω
35 4 34 eqbrtri 𝑍 ≼ ω
36 35 a1i ( 𝜑𝑍 ≼ ω )
37 7 simprd ( 𝜑Disj 𝑛𝑍 ( 𝐹𝑛 ) )
38 1 2 3 32 36 37 meadjiun ( 𝜑 → ( 𝑀 𝑛𝑍 ( 𝐹𝑛 ) ) = ( Σ^ ‘ ( 𝑛𝑍 ↦ ( 𝑀 ‘ ( 𝐹𝑛 ) ) ) ) )
39 eqidd ( 𝜑 → ( Σ^ ‘ ( 𝑛𝑍 ↦ ( 𝑀 ‘ ( 𝐹𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛𝑍 ↦ ( 𝑀 ‘ ( 𝐹𝑛 ) ) ) ) )
40 10 38 39 3eqtrd ( 𝜑 → ( 𝑀 𝑛𝑍 ( 𝐸𝑛 ) ) = ( Σ^ ‘ ( 𝑛𝑍 ↦ ( 𝑀 ‘ ( 𝐹𝑛 ) ) ) ) )
41 4 fvexi 𝑍 ∈ V
42 41 a1i ( 𝜑𝑍 ∈ V )
43 2 adantr ( ( 𝜑𝑛𝑍 ) → 𝑀 ∈ Meas )
44 43 3 32 meacl ( ( 𝜑𝑛𝑍 ) → ( 𝑀 ‘ ( 𝐹𝑛 ) ) ∈ ( 0 [,] +∞ ) )
45 43 3 13 meacl ( ( 𝜑𝑛𝑍 ) → ( 𝑀 ‘ ( 𝐸𝑛 ) ) ∈ ( 0 [,] +∞ ) )
46 simpr ( ( 𝜑𝑛𝑍 ) → 𝑛𝑍 )
47 13 difexd ( ( 𝜑𝑛𝑍 ) → ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) ∈ V )
48 6 fvmpt2 ( ( 𝑛𝑍 ∧ ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) ∈ V ) → ( 𝐹𝑛 ) = ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) )
49 46 47 48 syl2anc ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) = ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) )
50 difssd ( ( 𝜑𝑛𝑍 ) → ( ( 𝐸𝑛 ) ∖ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸𝑖 ) ) ⊆ ( 𝐸𝑛 ) )
51 49 50 eqsstrd ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) ⊆ ( 𝐸𝑛 ) )
52 43 3 32 13 51 meassle ( ( 𝜑𝑛𝑍 ) → ( 𝑀 ‘ ( 𝐹𝑛 ) ) ≤ ( 𝑀 ‘ ( 𝐸𝑛 ) ) )
53 1 42 44 45 52 sge0lempt ( 𝜑 → ( Σ^ ‘ ( 𝑛𝑍 ↦ ( 𝑀 ‘ ( 𝐹𝑛 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑛𝑍 ↦ ( 𝑀 ‘ ( 𝐸𝑛 ) ) ) ) )
54 40 53 eqbrtrd ( 𝜑 → ( 𝑀 𝑛𝑍 ( 𝐸𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛𝑍 ↦ ( 𝑀 ‘ ( 𝐸𝑛 ) ) ) ) )