Theorem meaiuninc3

Description: Measures are continuous from below: 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 the general case of Proposition 112C (e) of Fremlin1 p. 16 . This theorem generalizes meaiuninc and meaiuninc2 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022)

	Ref	Expression
Hypotheses	meaiuninc3.p	⊢ Ⅎ 𝑛 𝜑
	meaiuninc3.f	⊢ Ⅎ 𝑛 𝐸
	meaiuninc3.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meaiuninc3.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	meaiuninc3.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
	meaiuninc3.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
	meaiuninc3.i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) )
	meaiuninc3.s	⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
Assertion	meaiuninc3	⊢ ( 𝜑 → 𝑆 ~~>* ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		meaiuninc3.p	⊢ Ⅎ 𝑛 𝜑
2		meaiuninc3.f	⊢ Ⅎ 𝑛 𝐸
3		meaiuninc3.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
4		meaiuninc3.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5		meaiuninc3.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
6		meaiuninc3.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
7		meaiuninc3.i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) )
8		meaiuninc3.s	⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
9		nfv	⊢ Ⅎ 𝑛 𝑘 ∈ 𝑍
10	1 9	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑘 ∈ 𝑍 )
11		nfcv	⊢ Ⅎ 𝑛 𝑘
12	2 11	nffv	⊢ Ⅎ 𝑛 ( 𝐸 ‘ 𝑘 )
13		nfcv	⊢ Ⅎ 𝑛 ( 𝑘 + 1 )
14	2 13	nffv	⊢ Ⅎ 𝑛 ( 𝐸 ‘ ( 𝑘 + 1 ) )
15	12 14	nfss	⊢ Ⅎ 𝑛 ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) )
16	10 15	nfim	⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
17		eleq1w	⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ 𝑍 ↔ 𝑘 ∈ 𝑍 ) )
18	17	anbi2d	⊢ ( 𝑛 = 𝑘 → ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ) )
19		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑘 ) )
20		fvoveq1	⊢ ( 𝑛 = 𝑘 → ( 𝐸 ‘ ( 𝑛 + 1 ) ) = ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
21	19 20	sseq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) )
22	18 21	imbi12d	⊢ ( 𝑛 = 𝑘 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ) )
23	16 22 7	chvarfv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
24		nfcv	⊢ Ⅎ 𝑘 𝑀
25		nfcv	⊢ Ⅎ 𝑘 ( 𝐸 ‘ 𝑛 )
26	24 25	nffv	⊢ Ⅎ 𝑘 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) )
27		nfcv	⊢ Ⅎ 𝑛 𝑀
28	27 12	nffv	⊢ Ⅎ 𝑛 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) )
29		2fveq3	⊢ ( 𝑛 = 𝑘 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) )
30	26 28 29	cbvmpt	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) )
31	8 30	eqtri	⊢ 𝑆 = ( 𝑘 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) )
32	3 4 5 6 23 31	meaiuninc3v	⊢ ( 𝜑 → 𝑆 ~~>* ( 𝑀 ‘ ∪ 𝑘 ∈ 𝑍 ( 𝐸 ‘ 𝑘 ) ) )
33		fveq2	⊢ ( 𝑘 = 𝑛 → ( 𝐸 ‘ 𝑘 ) = ( 𝐸 ‘ 𝑛 ) )
34	12 25 33	cbviun	⊢ ∪ 𝑘 ∈ 𝑍 ( 𝐸 ‘ 𝑘 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 )
35	34	fveq2i	⊢ ( 𝑀 ‘ ∪ 𝑘 ∈ 𝑍 ( 𝐸 ‘ 𝑘 ) ) = ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
36	32 35	breqtrdi	⊢ ( 𝜑 → 𝑆 ~~>* ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )