Theorem meaiininc

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	meaiininc.f	⊢ Ⅎ 𝑛 𝜑
	meaiininc.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meaiininc.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	meaiininc.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
	meaiininc.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
	meaiininc.i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑛 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑛 ) )
	meaiininc.k	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) )
	meaiininc.r	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ‘ 𝐾 ) ) ∈ ℝ )
	meaiininc.s	⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
Assertion	meaiininc	⊢ ( 𝜑 → 𝑆 ⇝ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		meaiininc.f	⊢ Ⅎ 𝑛 𝜑
2		meaiininc.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
3		meaiininc.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		meaiininc.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
5		meaiininc.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
6		meaiininc.i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑛 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑛 ) )
7		meaiininc.k	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) )
8		meaiininc.r	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ‘ 𝐾 ) ) ∈ ℝ )
9		meaiininc.s	⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
10		nfv	⊢ Ⅎ 𝑛 𝑖 ∈ 𝑍
11	1 10	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑖 ∈ 𝑍 )
12		nfv	⊢ Ⅎ 𝑛 ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑖 )
13	11 12	nfim	⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑖 ) )
14		eleq1w	⊢ ( 𝑛 = 𝑖 → ( 𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍 ) )
15	14	anbi2d	⊢ ( 𝑛 = 𝑖 → ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ) )
16		fvoveq1	⊢ ( 𝑛 = 𝑖 → ( 𝐸 ‘ ( 𝑛 + 1 ) ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
17		fveq2	⊢ ( 𝑛 = 𝑖 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑖 ) )
18	16 17	sseq12d	⊢ ( 𝑛 = 𝑖 → ( ( 𝐸 ‘ ( 𝑛 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑛 ) ↔ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑖 ) ) )
19	15 18	imbi12d	⊢ ( 𝑛 = 𝑖 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑛 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑛 ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑖 ) ) ) )
20	13 19 6	chvarfv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑖 ) )
21		2fveq3	⊢ ( 𝑚 = 𝑖 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) )
22	21	cbvmptv	⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) = ( 𝑖 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) )
23	17	difeq2d	⊢ ( 𝑛 = 𝑖 → ( ( 𝐸 ‘ 𝐾 ) ∖ ( 𝐸 ‘ 𝑛 ) ) = ( ( 𝐸 ‘ 𝐾 ) ∖ ( 𝐸 ‘ 𝑖 ) ) )
24	23	cbvmptv	⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝐾 ) ∖ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑖 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝐾 ) ∖ ( 𝐸 ‘ 𝑖 ) ) )
25		fveq2	⊢ ( 𝑚 = 𝑖 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝐾 ) ∖ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝐾 ) ∖ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑖 ) )
26	25	cbviunv	⊢ ∪ 𝑚 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝐾 ) ∖ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ∪ 𝑖 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝐾 ) ∖ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑖 )
27	2 3 4 5 20 7 8 22 24 26	meaiininclem	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ⇝ ( 𝑀 ‘ ∩ 𝑖 ∈ 𝑍 ( 𝐸 ‘ 𝑖 ) ) )
28		2fveq3	⊢ ( 𝑛 = 𝑚 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) )
29	28	cbvmptv	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) )
30	9 29	eqtri	⊢ 𝑆 = ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) )
31	30	a1i	⊢ ( 𝜑 → 𝑆 = ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) )
32	17	cbviinv	⊢ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∩ 𝑖 ∈ 𝑍 ( 𝐸 ‘ 𝑖 )
33	32	fveq2i	⊢ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ∩ 𝑖 ∈ 𝑍 ( 𝐸 ‘ 𝑖 ) )
34	33	a1i	⊢ ( 𝜑 → ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ∩ 𝑖 ∈ 𝑍 ( 𝐸 ‘ 𝑖 ) ) )
35	31 34	breq12d	⊢ ( 𝜑 → ( 𝑆 ⇝ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ↔ ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ⇝ ( 𝑀 ‘ ∩ 𝑖 ∈ 𝑍 ( 𝐸 ‘ 𝑖 ) ) ) )
36	27 35	mpbird	⊢ ( 𝜑 → 𝑆 ⇝ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )