meaiininclem

Description: Measures are continuous from above: if E is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	meaiininclem.m	$⊢ φ \to M \in Meas$
	meaiininclem.n	$⊢ φ \to N \in ℤ$
	meaiininclem.z	$⊢ Z = ℤ_{\geq N}$
	meaiininclem.e	$⊢ φ \to E : Z ⟶ dom M$
	meaiininclem.i	$⊢ (φ \land n \in Z) \to E (n + 1) \subseteq E (n)$
	meaiininclem.k	$⊢ φ \to K \in ℤ_{\geq N}$
	meaiininclem.r	$⊢ φ \to M (E (K)) \in ℝ$
	meaiininclem.s	$⊢ S = (n \in Z ⟼ M (E (n)))$
	meaiininclem.g	$⊢ G = (n \in Z ⟼ E (K) ∖ E (n))$
	meaiininclem.f	$⊢ F = ⋃_{n \in Z} G (n)$
Assertion	meaiininclem	$⊢ φ \to S ⇝ M (⋂_{n \in Z} E (n))$

Proof

Step	Hyp	Ref	Expression
1		meaiininclem.m	$⊢ φ \to M \in Meas$
2		meaiininclem.n	$⊢ φ \to N \in ℤ$
3		meaiininclem.z	$⊢ Z = ℤ_{\geq N}$
4		meaiininclem.e	$⊢ φ \to E : Z ⟶ dom M$
5		meaiininclem.i	$⊢ (φ \land n \in Z) \to E (n + 1) \subseteq E (n)$
6		meaiininclem.k	$⊢ φ \to K \in ℤ_{\geq N}$
7		meaiininclem.r	$⊢ φ \to M (E (K)) \in ℝ$
8		meaiininclem.s	$⊢ S = (n \in Z ⟼ M (E (n)))$
9		meaiininclem.g	$⊢ G = (n \in Z ⟼ E (K) ∖ E (n))$
10		meaiininclem.f	$⊢ F = ⋃_{n \in Z} G (n)$
11		uzss	$⊢ K \in ℤ_{\geq N} \to ℤ_{\geq K} \subseteq ℤ_{\geq N}$
12	6 11	syl	$⊢ φ \to ℤ_{\geq K} \subseteq ℤ_{\geq N}$
13	12 3	sseqtrrdi	$⊢ φ \to ℤ_{\geq K} \subseteq Z$
14	13	adantr	$⊢ (φ \land n \in ℤ_{\geq K}) \to ℤ_{\geq K} \subseteq Z$
15		simpr	$⊢ (φ \land n \in ℤ_{\geq K}) \to n \in ℤ_{\geq K}$
16	14 15	sseldd	$⊢ (φ \land n \in ℤ_{\geq K}) \to n \in Z$
17	9	a1i	$⊢ φ \to G = (n \in Z ⟼ E (K) ∖ E (n))$
18		eqid	$⊢ dom M = dom M$
19	1 18	dmmeasal	$⊢ φ \to dom M \in SAlg$
20	19	adantr	$⊢ (φ \land n \in Z) \to dom M \in SAlg$
21	6 3	eleqtrrdi	$⊢ φ \to K \in Z$
22	4	ffvelrnda	$⊢ (φ \land K \in Z) \to E (K) \in dom M$
23	21 22	mpdan	$⊢ φ \to E (K) \in dom M$
24	23	adantr	$⊢ (φ \land n \in Z) \to E (K) \in dom M$
25	4	ffvelrnda	$⊢ (φ \land n \in Z) \to E (n) \in dom M$
26		saldifcl2	$⊢ (dom M \in SAlg \land E (K) \in dom M \land E (n) \in dom M) \to E (K) ∖ E (n) \in dom M$
27	20 24 25 26	syl3anc	$⊢ (φ \land n \in Z) \to E (K) ∖ E (n) \in dom M$
28	27	elexd	$⊢ (φ \land n \in Z) \to E (K) ∖ E (n) \in V$
29	17 28	fvmpt2d	$⊢ (φ \land n \in Z) \to G (n) = E (K) ∖ E (n)$
30	16 29	syldan	$⊢ (φ \land n \in ℤ_{\geq K}) \to G (n) = E (K) ∖ E (n)$
31	30	fveq2d	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (G (n)) = M (E (K) ∖ E (n))$
32	1	adantr	$⊢ (φ \land n \in ℤ_{\geq K}) \to M \in Meas$
33	23	adantr	$⊢ (φ \land n \in ℤ_{\geq K}) \to E (K) \in dom M$
34	7	adantr	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (E (K)) \in ℝ$
35	16 25	syldan	$⊢ (φ \land n \in ℤ_{\geq K}) \to E (n) \in dom M$
36		simpl	$⊢ (φ \land m \in (K ..^n)) \to φ$
37	36 13	syl	$⊢ (φ \land m \in (K ..^n)) \to ℤ_{\geq K} \subseteq Z$
38		elfzouz	$⊢ m \in (K ..^n) \to m \in ℤ_{\geq K}$
39	38	adantl	$⊢ (φ \land m \in (K ..^n)) \to m \in ℤ_{\geq K}$
40	37 39	sseldd	$⊢ (φ \land m \in (K ..^n)) \to m \in Z$
41		eleq1w	$⊢ n = m \to (n \in Z \leftrightarrow m \in Z)$
42	41	anbi2d	$⊢ n = m \to ((φ \land n \in Z) \leftrightarrow (φ \land m \in Z))$
43		fvoveq1	$⊢ n = m \to E (n + 1) = E (m + 1)$
44		fveq2	$⊢ n = m \to E (n) = E (m)$
45	43 44	sseq12d	$⊢ n = m \to (E (n + 1) \subseteq E (n) \leftrightarrow E (m + 1) \subseteq E (m))$
46	42 45	imbi12d	$⊢ n = m \to (((φ \land n \in Z) \to E (n + 1) \subseteq E (n)) \leftrightarrow ((φ \land m \in Z) \to E (m + 1) \subseteq E (m)))$
47	46 5	chvarvv	$⊢ (φ \land m \in Z) \to E (m + 1) \subseteq E (m)$
48	36 40 47	syl2anc	$⊢ (φ \land m \in (K ..^n)) \to E (m + 1) \subseteq E (m)$
49	48	adantlr	$⊢ ((φ \land n \in ℤ_{\geq K}) \land m \in (K ..^n)) \to E (m + 1) \subseteq E (m)$
50	15 49	ssdec	$⊢ (φ \land n \in ℤ_{\geq K}) \to E (n) \subseteq E (K)$
51	32 33 34 35 50	meadif	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (E (K) ∖ E (n)) = M (E (K)) - M (E (n))$
52	31 51	eqtrd	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (G (n)) = M (E (K)) - M (E (n))$
53	52	oveq2d	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (E (K)) - M (G (n)) = M (E (K)) - (M (E (K)) - M (E (n)))$
54	7	recnd	$⊢ φ \to M (E (K)) \in ℂ$
55	54	adantr	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (E (K)) \in ℂ$
56	32 33 34 50 35	meassre	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (E (n)) \in ℝ$
57	56	recnd	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (E (n)) \in ℂ$
58	55 57	nncand	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (E (K)) - (M (E (K)) - M (E (n))) = M (E (n))$
59	53 58	eqtr2d	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (E (n)) = M (E (K)) - M (G (n))$
60	59	mpteq2dva	$⊢ φ \to (n \in ℤ_{\geq K} ⟼ M (E (n))) = (n \in ℤ_{\geq K} ⟼ M (E (K)) - M (G (n)))$
61		nfv	$⊢ Ⅎ n φ$
62		eqid	$⊢ ℤ_{\geq K} = ℤ_{\geq K}$
63	6	eluzelzd	$⊢ φ \to K \in ℤ$
64		difssd	$⊢ (φ \land n \in Z) \to E (K) ∖ E (n) \subseteq E (K)$
65	29 64	eqsstrd	$⊢ (φ \land n \in Z) \to G (n) \subseteq E (K)$
66	16 65	syldan	$⊢ (φ \land n \in ℤ_{\geq K}) \to G (n) \subseteq E (K)$
67	27 9	fmptd	$⊢ φ \to G : Z ⟶ dom M$
68	67	ffvelrnda	$⊢ (φ \land n \in Z) \to G (n) \in dom M$
69	16 68	syldan	$⊢ (φ \land n \in ℤ_{\geq K}) \to G (n) \in dom M$
70	32 33 34 66 69	meassre	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (G (n)) \in ℝ$
71	70	recnd	$⊢ (φ \land n \in ℤ_{\geq K}) \to M (G (n)) \in ℂ$
72	5	sscond	$⊢ (φ \land n \in Z) \to E (K) ∖ E (n) \subseteq E (K) ∖ E (n + 1)$
73	44	difeq2d	$⊢ n = m \to E (K) ∖ E (n) = E (K) ∖ E (m)$
74	73	cbvmptv	$⊢ (n \in Z ⟼ E (K) ∖ E (n)) = (m \in Z ⟼ E (K) ∖ E (m))$
75	9 74	eqtri	$⊢ G = (m \in Z ⟼ E (K) ∖ E (m))$
76		fveq2	$⊢ m = n + 1 \to E (m) = E (n + 1)$
77	76	difeq2d	$⊢ m = n + 1 \to E (K) ∖ E (m) = E (K) ∖ E (n + 1)$
78	3	peano2uzs	$⊢ n \in Z \to n + 1 \in Z$
79	78	adantl	$⊢ (φ \land n \in Z) \to n + 1 \in Z$
80		fvex	$⊢ E (K) \in V$
81	80	difexi	$⊢ E (K) ∖ E (n + 1) \in V$
82	81	a1i	$⊢ (φ \land n \in Z) \to E (K) ∖ E (n + 1) \in V$
83	75 77 79 82	fvmptd3	$⊢ (φ \land n \in Z) \to G (n + 1) = E (K) ∖ E (n + 1)$
84	29 83	sseq12d	$⊢ (φ \land n \in Z) \to (G (n) \subseteq G (n + 1) \leftrightarrow E (K) ∖ E (n) \subseteq E (K) ∖ E (n + 1))$
85	72 84	mpbird	$⊢ (φ \land n \in Z) \to G (n) \subseteq G (n + 1)$
86	1	adantr	$⊢ (φ \land n \in Z) \to M \in Meas$
87	86 18 68 24 65	meassle	$⊢ (φ \land n \in Z) \to M (G (n)) \leq M (E (K))$
88		eqid	$⊢ (n \in Z ⟼ M (G (n))) = (n \in Z ⟼ M (G (n)))$
89	1 2 3 67 85 7 87 88	meaiuninc2	$⊢ φ \to (n \in Z ⟼ M (G (n))) ⇝ M (⋃_{n \in Z} G (n))$
90		eqid	$⊢ (n \in ℤ_{\geq K} ⟼ M (G (n))) = (n \in ℤ_{\geq K} ⟼ M (G (n)))$
91	3 88 21 90	climresmpt	$⊢ φ \to ((n \in ℤ_{\geq K} ⟼ M (G (n))) ⇝ M (⋃_{n \in Z} G (n)) \leftrightarrow (n \in Z ⟼ M (G (n))) ⇝ M (⋃_{n \in Z} G (n)))$
92	89 91	mpbird	$⊢ φ \to (n \in ℤ_{\geq K} ⟼ M (G (n))) ⇝ M (⋃_{n \in Z} G (n))$
93	10	eqcomi	$⊢ ⋃_{n \in Z} G (n) = F$
94	93	fveq2i	$⊢ M (⋃_{n \in Z} G (n)) = M (F)$
95	94	a1i	$⊢ φ \to M (⋃_{n \in Z} G (n)) = M (F)$
96	92 95	breqtrd	$⊢ φ \to (n \in ℤ_{\geq K} ⟼ M (G (n))) ⇝ M (F)$
97	61 62 63 54 71 96	climsubc1mpt	$⊢ φ \to (n \in ℤ_{\geq K} ⟼ M (E (K)) - M (G (n))) ⇝ (M (E (K)) - M (F))$
98	60 97	eqbrtrd	$⊢ φ \to (n \in ℤ_{\geq K} ⟼ M (E (n))) ⇝ (M (E (K)) - M (F))$
99		eqid	$⊢ (n \in Z ⟼ M (E (n))) = (n \in Z ⟼ M (E (n)))$
100		eqid	$⊢ (n \in ℤ_{\geq K} ⟼ M (E (n))) = (n \in ℤ_{\geq K} ⟼ M (E (n)))$
101	3 99 21 100	climresmpt	$⊢ φ \to ((n \in ℤ_{\geq K} ⟼ M (E (n))) ⇝ (M (E (K)) - M (F)) \leftrightarrow (n \in Z ⟼ M (E (n))) ⇝ (M (E (K)) - M (F)))$
102	98 101	mpbid	$⊢ φ \to (n \in Z ⟼ M (E (n))) ⇝ (M (E (K)) - M (F))$
103	8	a1i	$⊢ φ \to S = (n \in Z ⟼ M (E (n)))$
104		eqidd	$⊢ φ \to M (F \cup (E (K) ∖ F)) = M (F \cup (E (K) ∖ F))$
105	3	uzct	$⊢ Z ≼ ω$
106	105	a1i	$⊢ φ \to Z ≼ ω$
107	19 106 68	saliuncl	$⊢ φ \to ⋃_{n \in Z} G (n) \in dom M$
108	10 107	eqeltrid	$⊢ φ \to F \in dom M$
109		saldifcl2	$⊢ (dom M \in SAlg \land E (K) \in dom M \land F \in dom M) \to E (K) ∖ F \in dom M$
110	19 23 108 109	syl3anc	$⊢ φ \to E (K) ∖ F \in dom M$
111		disjdif	$⊢ F \cap (E (K) ∖ F) = \emptyset$
112	111	a1i	$⊢ φ \to F \cap (E (K) ∖ F) = \emptyset$
113	65	iunssd	$⊢ φ \to ⋃_{n \in Z} G (n) \subseteq E (K)$
114	10 113	eqsstrid	$⊢ φ \to F \subseteq E (K)$
115	1 23 7 114 108	meassre	$⊢ φ \to M (F) \in ℝ$
116		difssd	$⊢ φ \to E (K) ∖ F \subseteq E (K)$
117	1 23 7 116 110	meassre	$⊢ φ \to M (E (K) ∖ F) \in ℝ$
118	1 18 108 110 112 115 117	meadjunre	$⊢ φ \to M (F \cup (E (K) ∖ F)) = M (F) + M (E (K) ∖ F)$
119		undif	$⊢ F \subseteq E (K) \leftrightarrow F \cup (E (K) ∖ F) = E (K)$
120	114 119	sylib	$⊢ φ \to F \cup (E (K) ∖ F) = E (K)$
121	120	fveq2d	$⊢ φ \to M (F \cup (E (K) ∖ F)) = M (E (K))$
122	104 118 121	3eqtr3d	$⊢ φ \to M (F) + M (E (K) ∖ F) = M (E (K))$
123	115	recnd	$⊢ φ \to M (F) \in ℂ$
124	117	recnd	$⊢ φ \to M (E (K) ∖ F) \in ℂ$
125	54 123 124	subaddd	$⊢ φ \to (M (E (K)) - M (F) = M (E (K) ∖ F) \leftrightarrow M (F) + M (E (K) ∖ F) = M (E (K)))$
126	122 125	mpbird	$⊢ φ \to M (E (K)) - M (F) = M (E (K) ∖ F)$
127		simpllr	$⊢ (((φ \land x \in (E (K) ∖ F)) \land n \in Z) \land \neg x \in E (n)) \to x \in (E (K) ∖ F)$
128		simplr	$⊢ ((x \in (E (K) ∖ F) \land n \in Z) \land \neg x \in E (n)) \to n \in Z$
129		eldifi	$⊢ x \in (E (K) ∖ F) \to x \in E (K)$
130	129	ad2antrr	$⊢ ((x \in (E (K) ∖ F) \land n \in Z) \land \neg x \in E (n)) \to x \in E (K)$
131		simpr	$⊢ ((x \in (E (K) ∖ F) \land n \in Z) \land \neg x \in E (n)) \to \neg x \in E (n)$
132	130 131	eldifd	$⊢ ((x \in (E (K) ∖ F) \land n \in Z) \land \neg x \in E (n)) \to x \in (E (K) ∖ E (n))$
133		rspe	$⊢ (n \in Z \land x \in (E (K) ∖ E (n))) \to \exists n \in Z x \in (E (K) ∖ E (n))$
134	128 132 133	syl2anc	$⊢ ((x \in (E (K) ∖ F) \land n \in Z) \land \neg x \in E (n)) \to \exists n \in Z x \in (E (K) ∖ E (n))$
135		eliun	$⊢ x \in ⋃_{n \in Z} (E (K) ∖ E (n)) \leftrightarrow \exists n \in Z x \in (E (K) ∖ E (n))$
136	134 135	sylibr	$⊢ ((x \in (E (K) ∖ F) \land n \in Z) \land \neg x \in E (n)) \to x \in ⋃_{n \in Z} (E (K) ∖ E (n))$
137	136	adantlll	$⊢ (((φ \land x \in (E (K) ∖ F)) \land n \in Z) \land \neg x \in E (n)) \to x \in ⋃_{n \in Z} (E (K) ∖ E (n))$
138	10	a1i	$⊢ φ \to F = ⋃_{n \in Z} G (n)$
139	29	iuneq2dv	$⊢ φ \to ⋃_{n \in Z} G (n) = ⋃_{n \in Z} (E (K) ∖ E (n))$
140	138 139	eqtrd	$⊢ φ \to F = ⋃_{n \in Z} (E (K) ∖ E (n))$
141	140	eqcomd	$⊢ φ \to ⋃_{n \in Z} (E (K) ∖ E (n)) = F$
142	141	ad3antrrr	$⊢ (((φ \land x \in (E (K) ∖ F)) \land n \in Z) \land \neg x \in E (n)) \to ⋃_{n \in Z} (E (K) ∖ E (n)) = F$
143	137 142	eleqtrd	$⊢ (((φ \land x \in (E (K) ∖ F)) \land n \in Z) \land \neg x \in E (n)) \to x \in F$
144		elndif	$⊢ x \in F \to \neg x \in (E (K) ∖ F)$
145	143 144	syl	$⊢ (((φ \land x \in (E (K) ∖ F)) \land n \in Z) \land \neg x \in E (n)) \to \neg x \in (E (K) ∖ F)$
146	127 145	condan	$⊢ ((φ \land x \in (E (K) ∖ F)) \land n \in Z) \to x \in E (n)$
147	146	ralrimiva	$⊢ (φ \land x \in (E (K) ∖ F)) \to \forall n \in Z x \in E (n)$
148		vex	$⊢ x \in V$
149		eliin	$⊢ x \in V \to (x \in ⋂_{n \in Z} E (n) \leftrightarrow \forall n \in Z x \in E (n))$
150	148 149	ax-mp	$⊢ x \in ⋂_{n \in Z} E (n) \leftrightarrow \forall n \in Z x \in E (n)$
151	147 150	sylibr	$⊢ (φ \land x \in (E (K) ∖ F)) \to x \in ⋂_{n \in Z} E (n)$
152	151	ssd	$⊢ φ \to E (K) ∖ F \subseteq ⋂_{n \in Z} E (n)$
153		ssid	$⊢ E (K) \subseteq E (K)$
154	153	a1i	$⊢ φ \to E (K) \subseteq E (K)$
155		fveq2	$⊢ n = K \to E (n) = E (K)$
156	155	sseq1d	$⊢ n = K \to (E (n) \subseteq E (K) \leftrightarrow E (K) \subseteq E (K))$
157	156	rspcev	$⊢ (K \in Z \land E (K) \subseteq E (K)) \to \exists n \in Z E (n) \subseteq E (K)$
158	21 154 157	syl2anc	$⊢ φ \to \exists n \in Z E (n) \subseteq E (K)$
159		iinss	$⊢ \exists n \in Z E (n) \subseteq E (K) \to ⋂_{n \in Z} E (n) \subseteq E (K)$
160	158 159	syl	$⊢ φ \to ⋂_{n \in Z} E (n) \subseteq E (K)$
161	160	adantr	$⊢ (φ \land x \in ⋂_{n \in Z} E (n)) \to ⋂_{n \in Z} E (n) \subseteq E (K)$
162		simpr	$⊢ (φ \land x \in ⋂_{n \in Z} E (n)) \to x \in ⋂_{n \in Z} E (n)$
163	161 162	sseldd	$⊢ (φ \land x \in ⋂_{n \in Z} E (n)) \to x \in E (K)$
164		nfcv	$⊢ \underline{Ⅎ} n x$
165		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} E (n)$
166	164 165	nfel	$⊢ Ⅎ n x \in ⋂_{n \in Z} E (n)$
167		iinss2	$⊢ n \in Z \to ⋂_{n \in Z} E (n) \subseteq E (n)$
168	167	adantl	$⊢ (x \in ⋂_{n \in Z} E (n) \land n \in Z) \to ⋂_{n \in Z} E (n) \subseteq E (n)$
169		simpl	$⊢ (x \in ⋂_{n \in Z} E (n) \land n \in Z) \to x \in ⋂_{n \in Z} E (n)$
170	168 169	sseldd	$⊢ (x \in ⋂_{n \in Z} E (n) \land n \in Z) \to x \in E (n)$
171		elndif	$⊢ x \in E (n) \to \neg x \in (E (K) ∖ E (n))$
172	170 171	syl	$⊢ (x \in ⋂_{n \in Z} E (n) \land n \in Z) \to \neg x \in (E (K) ∖ E (n))$
173	172	ex	$⊢ x \in ⋂_{n \in Z} E (n) \to (n \in Z \to \neg x \in (E (K) ∖ E (n)))$
174	166 173	ralrimi	$⊢ x \in ⋂_{n \in Z} E (n) \to \forall n \in Z \neg x \in (E (K) ∖ E (n))$
175		ralnex	$⊢ \forall n \in Z \neg x \in (E (K) ∖ E (n)) \leftrightarrow \neg \exists n \in Z x \in (E (K) ∖ E (n))$
176	174 175	sylib	$⊢ x \in ⋂_{n \in Z} E (n) \to \neg \exists n \in Z x \in (E (K) ∖ E (n))$
177	176 135	sylnibr	$⊢ x \in ⋂_{n \in Z} E (n) \to \neg x \in ⋃_{n \in Z} (E (K) ∖ E (n))$
178	177	adantl	$⊢ (φ \land x \in ⋂_{n \in Z} E (n)) \to \neg x \in ⋃_{n \in Z} (E (K) ∖ E (n))$
179	140	adantr	$⊢ (φ \land x \in ⋂_{n \in Z} E (n)) \to F = ⋃_{n \in Z} (E (K) ∖ E (n))$
180	178 179	neleqtrrd	$⊢ (φ \land x \in ⋂_{n \in Z} E (n)) \to \neg x \in F$
181	163 180	eldifd	$⊢ (φ \land x \in ⋂_{n \in Z} E (n)) \to x \in (E (K) ∖ F)$
182	152 181	eqelssd	$⊢ φ \to E (K) ∖ F = ⋂_{n \in Z} E (n)$
183	182	fveq2d	$⊢ φ \to M (E (K) ∖ F) = M (⋂_{n \in Z} E (n))$
184	126 183	eqtr2d	$⊢ φ \to M (⋂_{n \in Z} E (n)) = M (E (K)) - M (F)$
185	103 184	breq12d	$⊢ φ \to (S ⇝ M (⋂_{n \in Z} E (n)) \leftrightarrow (n \in Z ⟼ M (E (n))) ⇝ (M (E (K)) - M (F)))$
186	102 185	mpbird	$⊢ φ \to S ⇝ M (⋂_{n \in Z} E (n))$

Metamath Proof Explorer

Theorem meaiininclem

Proof