Theorem meaiunincf

Description: Measures are continuous from below (bounded case): if E is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 13-Feb-2022)

	Ref	Expression
Hypotheses	meaiunincf.p	⊢ Ⅎ 𝑛 𝜑
	meaiunincf.f	⊢ Ⅎ 𝑛 𝐸
	meaiunincf.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meaiunincf.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	meaiunincf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
	meaiunincf.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
	meaiunincf.i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) )
	meaiunincf.x	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
	meaiunincf.s	⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
Assertion	meaiunincf	⊢ ( 𝜑 → 𝑆 ⇝ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		meaiunincf.p	⊢ Ⅎ 𝑛 𝜑
2		meaiunincf.f	⊢ Ⅎ 𝑛 𝐸
3		meaiunincf.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
4		meaiunincf.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5		meaiunincf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
6		meaiunincf.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
7		meaiunincf.i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) )
8		meaiunincf.x	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
9		meaiunincf.s	⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
10		nfv	⊢ Ⅎ 𝑛 𝑘 ∈ 𝑍
11	1 10	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑘 ∈ 𝑍 )
12		nfcv	⊢ Ⅎ 𝑛 𝑘
13	2 12	nffv	⊢ Ⅎ 𝑛 ( 𝐸 ‘ 𝑘 )
14		nfcv	⊢ Ⅎ 𝑛 ( 𝑘 + 1 )
15	2 14	nffv	⊢ Ⅎ 𝑛 ( 𝐸 ‘ ( 𝑘 + 1 ) )
16	13 15	nfss	⊢ Ⅎ 𝑛 ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) )
17	11 16	nfim	⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
18		eleq1w	⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ 𝑍 ↔ 𝑘 ∈ 𝑍 ) )
19	18	anbi2d	⊢ ( 𝑛 = 𝑘 → ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ) )
20		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑘 ) )
21		fvoveq1	⊢ ( 𝑛 = 𝑘 → ( 𝐸 ‘ ( 𝑛 + 1 ) ) = ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
22	20 21	sseq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) )
23	19 22	imbi12d	⊢ ( 𝑛 = 𝑘 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ) )
24	17 23 7	chvarfv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
25		breq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑦 ) )
26	25	ralbidv	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑦 ) )
27		nfv	⊢ Ⅎ 𝑘 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑦
28		nfcv	⊢ Ⅎ 𝑛 𝑀
29	28 13	nffv	⊢ Ⅎ 𝑛 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) )
30		nfcv	⊢ Ⅎ 𝑛 ≤
31		nfcv	⊢ Ⅎ 𝑛 𝑦
32	29 30 31	nfbr	⊢ Ⅎ 𝑛 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ≤ 𝑦
33		2fveq3	⊢ ( 𝑛 = 𝑘 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) )
34	33	breq1d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑦 ↔ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ≤ 𝑦 ) )
35	27 32 34	cbvralw	⊢ ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑦 ↔ ∀ 𝑘 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ≤ 𝑦 )
36	35	a1i	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑦 ↔ ∀ 𝑘 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ≤ 𝑦 ) )
37	26 36	bitrd	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ≤ 𝑦 ) )
38	37	cbvrexvw	⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ≤ 𝑦 )
39	8 38	sylib	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ≤ 𝑦 )
40		nfcv	⊢ Ⅎ 𝑘 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) )
41	40 29 33	cbvmpt	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) )
42	9 41	eqtri	⊢ 𝑆 = ( 𝑘 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) )
43	3 4 5 6 24 39 42	meaiuninc	⊢ ( 𝜑 → 𝑆 ⇝ ( 𝑀 ‘ ∪ 𝑘 ∈ 𝑍 ( 𝐸 ‘ 𝑘 ) ) )
44		nfcv	⊢ Ⅎ 𝑘 ( 𝐸 ‘ 𝑛 )
45		fveq2	⊢ ( 𝑘 = 𝑛 → ( 𝐸 ‘ 𝑘 ) = ( 𝐸 ‘ 𝑛 ) )
46	13 44 45	cbviun	⊢ ∪ 𝑘 ∈ 𝑍 ( 𝐸 ‘ 𝑘 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 )
47	46	fveq2i	⊢ ( 𝑀 ‘ ∪ 𝑘 ∈ 𝑍 ( 𝐸 ‘ 𝑘 ) ) = ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
48	43 47	breqtrdi	⊢ ( 𝜑 → 𝑆 ⇝ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )