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 ⊢ Ⅎ n φ
meaiunlelem.m ⊢ φ → M ∈ Meas
meaiunlelem.s ⊢ S = dom ⁡ M
meaiunlelem.z ⊢ Z = ℤ ≥ N
meaiunlelem.e ⊢ φ → E : Z ⟶ S
meaiunlelem.f ⊢ F = n ∈ Z ⟼ E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i
Assertion meaiunlelem ⊢ φ → M ⁡ ⋃ n ∈ Z E ⁡ n ≤ sum^ ⁡ n ∈ Z ⟼ M ⁡ E ⁡ n

Proof

Step Hyp Ref Expression
1 meaiunlelem.1 ⊢ Ⅎ n φ
2 meaiunlelem.m ⊢ φ → M ∈ Meas
3 meaiunlelem.s ⊢ S = dom ⁡ M
4 meaiunlelem.z ⊢ Z = ℤ ≥ N
5 meaiunlelem.e ⊢ φ → E : Z ⟶ S
6 meaiunlelem.f ⊢ F = n ∈ Z ⟼ E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i
7 1 4 5 6 iundjiun ⊢ φ → ∀ x ∈ Z ⋃ n = N x F ⁡ n = ⋃ n = N x E ⁡ n ∧ ⋃ n ∈ Z F ⁡ n = ⋃ n ∈ Z E ⁡ n ∧ Disj n ∈ Z F ⁡ n
8 7 simplrd ⊢ φ → ⋃ n ∈ Z F ⁡ n = ⋃ n ∈ Z E ⁡ n
9 8 eqcomd ⊢ φ → ⋃ n ∈ Z E ⁡ n = ⋃ n ∈ Z F ⁡ n
10 9 fveq2d ⊢ φ → M ⁡ ⋃ n ∈ Z E ⁡ n = M ⁡ ⋃ n ∈ Z F ⁡ n
11 2 3 dmmeasal ⊢ φ → S ∈ SAlg
12 11 adantr ⊢ φ ∧ n ∈ Z → S ∈ SAlg
13 5 ffvelcdmda ⊢ φ ∧ n ∈ Z → E ⁡ n ∈ S
14 fzofi ⊢ N ..^ n ∈ Fin
15 isfinite ⊢ N ..^ n ∈ Fin ↔ N ..^ n ≺ ω
16 15 biimpi ⊢ N ..^ n ∈ Fin → N ..^ n ≺ ω
17 sdomdom ⊢ N ..^ n ≺ ω → N ..^ n ≼ ω
18 16 17 syl ⊢ N ..^ n ∈ Fin → N ..^ n ≼ ω
19 14 18 ax-mp ⊢ N ..^ n ≼ ω
20 19 a1i ⊢ φ → N ..^ n ≼ ω
21 5 adantr ⊢ φ ∧ i ∈ N ..^ n → E : Z ⟶ S
22 elfzouz ⊢ i ∈ N ..^ n → i ∈ ℤ ≥ N
23 4 eqcomi ⊢ ℤ ≥ N = Z
24 22 23 eleqtrdi ⊢ i ∈ N ..^ n → i ∈ Z
25 24 adantl ⊢ φ ∧ i ∈ N ..^ n → i ∈ Z
26 21 25 ffvelcdmd ⊢ φ ∧ i ∈ N ..^ n → E ⁡ i ∈ S
27 11 20 26 saliuncl ⊢ φ → ⋃ i ∈ N ..^ n E ⁡ i ∈ S
28 27 adantr ⊢ φ ∧ n ∈ Z → ⋃ i ∈ N ..^ n E ⁡ i ∈ S
29 saldifcl2 ⊢ S ∈ SAlg ∧ E ⁡ n ∈ S ∧ ⋃ i ∈ N ..^ n E ⁡ i ∈ S → E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i ∈ S
30 12 13 28 29 syl3anc ⊢ φ ∧ n ∈ Z → E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i ∈ S
31 1 30 6 fmptdf ⊢ φ → F : Z ⟶ S
32 31 ffvelcdmda ⊢ φ ∧ n ∈ Z → F ⁡ n ∈ S
33 eqid ⊢ ℤ ≥ N = ℤ ≥ N
34 33 uzct ⊢ ℤ ≥ N ≼ ω
35 4 34 eqbrtri ⊢ Z ≼ ω
36 35 a1i ⊢ φ → Z ≼ ω
37 7 simprd ⊢ φ → Disj n ∈ Z F ⁡ n
38 1 2 3 32 36 37 meadjiun ⊢ φ → M ⁡ ⋃ n ∈ Z F ⁡ n = sum^ ⁡ n ∈ Z ⟼ M ⁡ F ⁡ n
39 eqidd ⊢ φ → sum^ ⁡ n ∈ Z ⟼ M ⁡ F ⁡ n = sum^ ⁡ n ∈ Z ⟼ M ⁡ F ⁡ n
40 10 38 39 3eqtrd ⊢ φ → M ⁡ ⋃ n ∈ Z E ⁡ n = sum^ ⁡ n ∈ Z ⟼ M ⁡ F ⁡ n
41 4 fvexi ⊢ Z ∈ V
42 41 a1i ⊢ φ → Z ∈ V
43 2 adantr ⊢ φ ∧ n ∈ Z → M ∈ Meas
44 43 3 32 meacl ⊢ φ ∧ n ∈ Z → M ⁡ F ⁡ n ∈ 0 +∞
45 43 3 13 meacl ⊢ φ ∧ n ∈ Z → M ⁡ E ⁡ n ∈ 0 +∞
46 simpr ⊢ φ ∧ n ∈ Z → n ∈ Z
47 13 difexd ⊢ φ ∧ n ∈ Z → E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i ∈ V
48 6 fvmpt2 ⊢ n ∈ Z ∧ E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i ∈ V → F ⁡ n = E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i
49 46 47 48 syl2anc ⊢ φ ∧ n ∈ Z → F ⁡ n = E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i
50 difssd ⊢ φ ∧ n ∈ Z → E ⁡ n ∖ ⋃ i ∈ N ..^ n E ⁡ i ⊆ E ⁡ n
51 49 50 eqsstrd ⊢ φ ∧ n ∈ Z → F ⁡ n ⊆ E ⁡ n
52 43 3 32 13 51 meassle ⊢ φ ∧ n ∈ Z → M ⁡ F ⁡ n ≤ M ⁡ E ⁡ n
53 1 42 44 45 52 sge0lempt ⊢ φ → sum^ ⁡ n ∈ Z ⟼ M ⁡ F ⁡ n ≤ sum^ ⁡ n ∈ Z ⟼ M ⁡ E ⁡ n
54 40 53 eqbrtrd ⊢ φ → M ⁡ ⋃ n ∈ Z E ⁡ n ≤ sum^ ⁡ n ∈ Z ⟼ M ⁡ E ⁡ n