Metamath Proof Explorer

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 = ( ZZ>= ` M )
mbfulm.m 
|- ( ph -> M e. ZZ )
mbfulm.f 
|- ( ph -> F : Z --> MblFn )
mbfulm.u 
|- ( ph -> F ( ~~>u ` S ) G )
Assertion mbfulm 
|- ( ph -> G e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfulm.z 
 |-  Z = ( ZZ>= ` M )
2 mbfulm.m 
 |-  ( ph -> M e. ZZ )
3 mbfulm.f 
 |-  ( ph -> F : Z --> MblFn )
4 mbfulm.u 
 |-  ( ph -> F ( ~~>u ` S ) G )
5 ulmcl 
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
6 4 5 syl 
 |-  ( ph -> G : S --> CC )
7 6 feqmptd 
 |-  ( ph -> G = ( z e. S |-> ( G ` z ) ) )
8 2 adantr 
 |-  ( ( ph /\ z e. S ) -> M e. ZZ )
9 3 ffnd 
 |-  ( ph -> F Fn Z )
10 ulmf2 
 |-  ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> F : Z --> ( CC ^m S ) )
11 9 4 10 syl2anc 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
12 11 adantr 
 |-  ( ( ph /\ z e. S ) -> F : Z --> ( CC ^m S ) )
13 simpr 
 |-  ( ( ph /\ z e. S ) -> z e. S )
14 1 fvexi 
 |-  Z e. _V
15 14 mptex 
 |-  ( k e. Z |-> ( ( F ` k ) ` z ) ) e. _V
16 15 a1i 
 |-  ( ( ph /\ z e. S ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) e. _V )
17 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
18 17 fveq1d 
 |-  ( k = n -> ( ( F ` k ) ` z ) = ( ( F ` n ) ` z ) )
19 eqid 
 |-  ( k e. Z |-> ( ( F ` k ) ` z ) ) = ( k e. Z |-> ( ( F ` k ) ` z ) )
20 fvex 
 |-  ( ( F ` n ) ` z ) e. _V
21 18 19 20 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ` n ) = ( ( F ` n ) ` z ) )
22 21 eqcomd 
 |-  ( n e. Z -> ( ( F ` n ) ` z ) = ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ` n ) )
23 22 adantl 
 |-  ( ( ( ph /\ z e. S ) /\ n e. Z ) -> ( ( F ` n ) ` z ) = ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ` n ) )
24 4 adantr 
 |-  ( ( ph /\ z e. S ) -> F ( ~~>u ` S ) G )
25 1 8 12 13 16 23 24 ulmclm 
 |-  ( ( ph /\ z e. S ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
26 11 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) )
27 elmapi 
 |-  ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
28 26 27 syl 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) : S --> CC )
29 28 feqmptd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( z e. S |-> ( ( F ` k ) ` z ) ) )
30 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. MblFn )
31 29 30 eqeltrrd 
 |-  ( ( ph /\ k e. Z ) -> ( z e. S |-> ( ( F ` k ) ` z ) ) e. MblFn )
32 28 ffvelcdmda 
 |-  ( ( ( ph /\ k e. Z ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC )
33 32 anasss 
 |-  ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) e. CC )
34 1 2 25 31 33 mbflim 
 |-  ( ph -> ( z e. S |-> ( G ` z ) ) e. MblFn )
35 7 34 eqeltrd 
 |-  ( ph -> G e. MblFn )