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	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	mbfulm.m	$$⊢\phi \to M\in \mathbb{Z}$$
	mbfulm.f	$$⊢\phi \to F:Z⟶MblFn$$
	mbfulm.u	$$⊢\phi \to F\underset{u}{⇝}\left(S\right)G$$
Assertion	mbfulm	$$⊢\phi \to G\in MblFn$$

Proof

Step	Hyp	Ref	Expression
1		mbfulm.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		mbfulm.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		mbfulm.f	$$⊢\phi \to F:Z⟶MblFn$$
4		mbfulm.u	$$⊢\phi \to F\underset{u}{⇝}\left(S\right)G$$
5		ulmcl	$$⊢F\underset{u}{⇝}\left(S\right)G\to G:S⟶ℂ$$
6	4 5	syl	$$⊢\phi \to G:S⟶ℂ$$
7	6	feqmptd	$$⊢\phi \to G=\left(z\in S⟼G\left(z\right)\right)$$
8	2	adantr	$$⊢\left(\phi \wedge z\in S\right)\to M\in \mathbb{Z}$$
9	3	ffnd	$$⊢\phi \to FFnZ$$
10		ulmf2	$$⊢\left(FFnZ\wedge F\underset{u}{⇝}\left(S\right)G\right)\to F:Z⟶{ℂ}^S$$
11	9 4 10	syl2anc	$$⊢\phi \to F:Z⟶{ℂ}^S$$
12	11	adantr	$$⊢\left(\phi \wedge z\in S\right)\to F:Z⟶{ℂ}^S$$
13		simpr	$$⊢\left(\phi \wedge z\in S\right)\to z\in S$$
14	1	fvexi	$$⊢Z\in \mathrm{V}$$
15	14	mptex	$$⊢\left(k\in Z⟼F\left(k\right)\left(z\right)\right)\in \mathrm{V}$$
16	15	a1i	$$⊢\left(\phi \wedge z\in S\right)\to \left(k\in Z⟼F\left(k\right)\left(z\right)\right)\in \mathrm{V}$$
17		fveq2	$$⊢k=n\to F\left(k\right)=F\left(n\right)$$
18	17	fveq1d	$$⊢k=n\to F\left(k\right)\left(z\right)=F\left(n\right)\left(z\right)$$
19		eqid	$$⊢\left(k\in Z⟼F\left(k\right)\left(z\right)\right)=\left(k\in Z⟼F\left(k\right)\left(z\right)\right)$$
20		fvex	$$⊢F\left(n\right)\left(z\right)\in \mathrm{V}$$
21	18 19 20	fvmpt	$$⊢n\in Z\to \left(k\in Z⟼F\left(k\right)\left(z\right)\right)\left(n\right)=F\left(n\right)\left(z\right)$$
22	21	eqcomd	$$⊢n\in Z\to F\left(n\right)\left(z\right)=\left(k\in Z⟼F\left(k\right)\left(z\right)\right)\left(n\right)$$
23	22	adantl	$$⊢\left(\left(\phi \wedge z\in S\right)\wedge n\in Z\right)\to F\left(n\right)\left(z\right)=\left(k\in Z⟼F\left(k\right)\left(z\right)\right)\left(n\right)$$
24	4	adantr	$$⊢\left(\phi \wedge z\in S\right)\to F\underset{u}{⇝}\left(S\right)G$$
25	1 8 12 13 16 23 24	ulmclm	$$⊢\left(\phi \wedge z\in S\right)\to \left(k\in Z⟼F\left(k\right)\left(z\right)\right)⇝G\left(z\right)$$
26	11	ffvelrnda	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in \left({ℂ}^S\right)$$
27		elmapi	$$⊢F\left(k\right)\in \left({ℂ}^S\right)\to F\left(k\right):S⟶ℂ$$
28	26 27	syl	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right):S⟶ℂ$$
29	28	feqmptd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=\left(z\in S⟼F\left(k\right)\left(z\right)\right)$$
30	3	ffvelrnda	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in MblFn$$
31	29 30	eqeltrrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left(z\in S⟼F\left(k\right)\left(z\right)\right)\in MblFn$$
32	28	ffvelrnda	$$⊢\left(\left(\phi \wedge k\in Z\right)\wedge z\in S\right)\to F\left(k\right)\left(z\right)\in ℂ$$
33	32	anasss	$$⊢\left(\phi \wedge \left(k\in Z\wedge z\in S\right)\right)\to F\left(k\right)\left(z\right)\in ℂ$$
34	1 2 25 31 33	mbflim	$$⊢\phi \to \left(z\in S⟼G\left(z\right)\right)\in MblFn$$
35	7 34	eqeltrd	$$⊢\phi \to G\in MblFn$$