Theorem mbfulm

Description: A uniform limit of measurable functions is measurable. (This is just a corollary of the fact that a pointwise limit of measurable functions is measurable, see mbflim .) (Contributed by Mario Carneiro, 18-Mar-2015)

	Ref	Expression
Hypotheses	mbfulm.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	mbfulm.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	mbfulm.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ MblFn )
	mbfulm.u	⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
Assertion	mbfulm	⊢ ( 𝜑 → 𝐺 ∈ MblFn )

Proof

Step	Hyp	Ref	Expression
1		mbfulm.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		mbfulm.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		mbfulm.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ MblFn )
4		mbfulm.u	⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
5		ulmcl	⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
6	4 5	syl	⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
7	6	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑧 ) ) )
8	2	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑀 ∈ ℤ )
9	3	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
10		ulmf2	⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
11	9 4 10	syl2anc	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
14	1	fvexi	⊢ 𝑍 ∈ V
15	14	mptex	⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ V
16	15	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ V )
17		fveq2	⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
18	17	fveq1d	⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) )
19		eqid	⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
20		fvex	⊢ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ∈ V
21	18 19 20	fvmpt	⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) )
22	21	eqcomd	⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
23	22	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
24	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
25	1 8 12 13 16 23 24	ulmclm	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
26	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
27		elmapi	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
28	26 27	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
29	28	feqmptd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝑧 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
30	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ MblFn )
31	29 30	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑧 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ MblFn )
32	28	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
33	32	anasss	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
34	1 2 25 31 33	mbflim	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ MblFn )
35	7 34	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ MblFn )