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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( ( 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 )