Metamath Proof Explorer

Theorem mbflimlem

Description: The pointwise limit of a sequence of measurable real-valued 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 )
mbflimlem.6 
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
Assertion mbflimlem 
|- ( 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 mbflimlem.6 
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
6 5 anass1rs 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. RR )
7 6 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) : Z --> RR )
8 2 adantr 
 |-  ( ( ph /\ x e. A ) -> M e. ZZ )
9 climrel 
 |-  Rel ~~>
10 9 releldmi 
 |-  ( ( n e. Z |-> B ) ~~> C -> ( n e. Z |-> B ) e. dom ~~> )
11 3 10 syl 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) e. dom ~~> )
12 1 climcau 
 |-  ( ( M e. ZZ /\ ( n e. Z |-> B ) e. dom ~~> ) -> A. y e. RR+ E. k e. Z A. j e. ( ZZ>= ` k ) ( abs ` ( ( ( n e. Z |-> B ) ` j ) - ( ( n e. Z |-> B ) ` k ) ) ) < y )
13 8 11 12 syl2anc 
 |-  ( ( ph /\ x e. A ) -> A. y e. RR+ E. k e. Z A. j e. ( ZZ>= ` k ) ( abs ` ( ( ( n e. Z |-> B ) ` j ) - ( ( n e. Z |-> B ) ` k ) ) ) < y )
14 1 7 13 caurcvg 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) ~~> ( limsup ` ( n e. Z |-> B ) ) )
15 climuni 
 |-  ( ( ( n e. Z |-> B ) ~~> ( limsup ` ( n e. Z |-> B ) ) /\ ( n e. Z |-> B ) ~~> C ) -> ( limsup ` ( n e. Z |-> B ) ) = C )
16 14 3 15 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) = C )
17 16 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( limsup ` ( n e. Z |-> B ) ) ) = ( x e. A |-> C ) )
18 eqid 
 |-  ( x e. A |-> ( limsup ` ( n e. Z |-> B ) ) ) = ( x e. A |-> ( limsup ` ( n e. Z |-> B ) ) )
19 eqid 
 |-  ( m e. RR |-> sup ( ( ( ( n e. Z |-> B ) " ( m [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( m e. RR |-> sup ( ( ( ( n e. Z |-> B ) " ( m [,) +oo ) ) i^i RR* ) , RR* , < ) )
20 7 ffvelrnda 
 |-  ( ( ( ph /\ x e. A ) /\ k e. Z ) -> ( ( n e. Z |-> B ) ` k ) e. RR )
21 1 8 14 20 climrecl 
 |-  ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) e. RR )
22 1 18 19 2 21 4 5 mbflimsup 
 |-  ( ph -> ( x e. A |-> ( limsup ` ( n e. Z |-> B ) ) ) e. MblFn )
23 17 22 eqeltrrd 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )