Metamath Proof Explorer

Theorem mbflim

Description: The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbflim.1 
|- Z = ( ZZ>= ` M )
mbflim.2 
|- ( ph -> M e. ZZ )
mbflim.4 
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) ~~> C )
mbflim.5 
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )
mbflim.6 
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. V )
Assertion mbflim 
|- ( ph -> ( x e. A |-> C ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbflim.1 
 |-  Z = ( ZZ>= ` M )
2 mbflim.2 
 |-  ( ph -> M e. ZZ )
3 mbflim.4 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) ~~> C )
4 mbflim.5 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )
5 mbflim.6 
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. V )
6 1 fvexi 
 |-  Z e. _V
7 6 mptex 
 |-  ( n e. Z |-> ( Re ` B ) ) e. _V
8 7 a1i 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> ( Re ` B ) ) e. _V )
9 2 adantr 
 |-  ( ( ph /\ x e. A ) -> M e. ZZ )
10 5 anassrs 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. V )
11 4 10 mbfmptcl 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. CC )
12 11 an32s 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. CC )
13 12 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) : Z --> CC )
14 13 ffvelrnda 
 |-  ( ( ( ph /\ x e. A ) /\ k e. Z ) -> ( ( n e. Z |-> B ) ` k ) e. CC )
15 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> n e. Z )
16 12 recld 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( Re ` B ) e. RR )
17 eqid 
 |-  ( n e. Z |-> ( Re ` B ) ) = ( n e. Z |-> ( Re ` B ) )
18 17 fvmpt2 
 |-  ( ( n e. Z /\ ( Re ` B ) e. RR ) -> ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` B ) )
19 15 16 18 syl2anc 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` B ) )
20 eqid 
 |-  ( n e. Z |-> B ) = ( n e. Z |-> B )
21 20 fvmpt2 
 |-  ( ( n e. Z /\ B e. CC ) -> ( ( n e. Z |-> B ) ` n ) = B )
22 15 12 21 syl2anc 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> B ) ` n ) = B )
23 22 fveq2d 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( Re ` ( ( n e. Z |-> B ) ` n ) ) = ( Re ` B ) )
24 19 23 eqtr4d 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) )
25 24 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. n e. Z ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) )
26 nffvmpt1 
 |-  F/_ n ( ( n e. Z |-> ( Re ` B ) ) ` k )
27 nfcv 
 |-  F/_ n Re
28 nffvmpt1 
 |-  F/_ n ( ( n e. Z |-> B ) ` k )
29 27 28 nffv 
 |-  F/_ n ( Re ` ( ( n e. Z |-> B ) ` k ) )
30 26 29 nfeq 
 |-  F/ n ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) )
31 nfv 
 |-  F/ k ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) )
32 fveq2 
 |-  ( k = n -> ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( ( n e. Z |-> ( Re ` B ) ) ` n ) )
33 2fveq3 
 |-  ( k = n -> ( Re ` ( ( n e. Z |-> B ) ` k ) ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) )
34 32 33 eqeq12d 
 |-  ( k = n -> ( ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) <-> ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) ) )
35 30 31 34 cbvralw 
 |-  ( A. k e. Z ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) <-> A. n e. Z ( ( n e. Z |-> ( Re ` B ) ) ` n ) = ( Re ` ( ( n e. Z |-> B ) ` n ) ) )
36 25 35 sylibr 
 |-  ( ( ph /\ x e. A ) -> A. k e. Z ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) )
37 36 r19.21bi 
 |-  ( ( ( ph /\ x e. A ) /\ k e. Z ) -> ( ( n e. Z |-> ( Re ` B ) ) ` k ) = ( Re ` ( ( n e. Z |-> B ) ` k ) ) )
38 1 3 8 9 14 37 climre 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> ( Re ` B ) ) ~~> ( Re ` C ) )
39 11 ismbfcn2 
 |-  ( ( ph /\ n e. Z ) -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) )
40 4 39 mpbid 
 |-  ( ( ph /\ n e. Z ) -> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) )
41 40 simpld 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> ( Re ` B ) ) e. MblFn )
42 11 anasss 
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. CC )
43 42 recld 
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> ( Re ` B ) e. RR )
44 1 2 38 41 43 mbflimlem 
 |-  ( ph -> ( x e. A |-> ( Re ` C ) ) e. MblFn )
45 6 mptex 
 |-  ( n e. Z |-> ( Im ` B ) ) e. _V
46 45 a1i 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> ( Im ` B ) ) e. _V )
47 12 imcld 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( Im ` B ) e. RR )
48 eqid 
 |-  ( n e. Z |-> ( Im ` B ) ) = ( n e. Z |-> ( Im ` B ) )
49 48 fvmpt2 
 |-  ( ( n e. Z /\ ( Im ` B ) e. RR ) -> ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` B ) )
50 15 47 49 syl2anc 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` B ) )
51 22 fveq2d 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( Im ` ( ( n e. Z |-> B ) ` n ) ) = ( Im ` B ) )
52 50 51 eqtr4d 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) )
53 52 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. n e. Z ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) )
54 nffvmpt1 
 |-  F/_ n ( ( n e. Z |-> ( Im ` B ) ) ` k )
55 nfcv 
 |-  F/_ n Im
56 55 28 nffv 
 |-  F/_ n ( Im ` ( ( n e. Z |-> B ) ` k ) )
57 54 56 nfeq 
 |-  F/ n ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) )
58 nfv 
 |-  F/ k ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) )
59 fveq2 
 |-  ( k = n -> ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( ( n e. Z |-> ( Im ` B ) ) ` n ) )
60 2fveq3 
 |-  ( k = n -> ( Im ` ( ( n e. Z |-> B ) ` k ) ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) )
61 59 60 eqeq12d 
 |-  ( k = n -> ( ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) <-> ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) ) )
62 57 58 61 cbvralw 
 |-  ( A. k e. Z ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) <-> A. n e. Z ( ( n e. Z |-> ( Im ` B ) ) ` n ) = ( Im ` ( ( n e. Z |-> B ) ` n ) ) )
63 53 62 sylibr 
 |-  ( ( ph /\ x e. A ) -> A. k e. Z ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) )
64 63 r19.21bi 
 |-  ( ( ( ph /\ x e. A ) /\ k e. Z ) -> ( ( n e. Z |-> ( Im ` B ) ) ` k ) = ( Im ` ( ( n e. Z |-> B ) ` k ) ) )
65 1 3 46 9 14 64 climim 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> ( Im ` B ) ) ~~> ( Im ` C ) )
66 40 simprd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> ( Im ` B ) ) e. MblFn )
67 42 imcld 
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> ( Im ` B ) e. RR )
68 1 2 65 66 67 mbflimlem 
 |-  ( ph -> ( x e. A |-> ( Im ` C ) ) e. MblFn )
69 climcl 
 |-  ( ( n e. Z |-> B ) ~~> C -> C e. CC )
70 3 69 syl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
71 70 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn <-> ( ( x e. A |-> ( Re ` C ) ) e. MblFn /\ ( x e. A |-> ( Im ` C ) ) e. MblFn ) ) )
72 44 68 71 mpbir2and 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )