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	$⊢ φ \to M \in Meas$
	meaiunlelem.s	$⊢ S = dom M$
	meaiunlelem.z	$⊢ Z = ℤ_{\geq N}$
	meaiunlelem.e	$⊢ φ \to E : Z ⟶ S$
	meaiunlelem.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
Assertion	meaiunlelem	$⊢ φ \to M (⋃_{n \in Z} E (n)) \leq sum^((n \in Z ⟼ M (E (n))))$

Proof

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

Metamath Proof Explorer

Theorem meaiunlelem

Proof