Metamath Proof Explorer

Theorem mbfi1flim

Description: Any real measurable function has a sequence of simple functions that converges to it. (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses mbfi1flim.1 
|- ( ph -> F e. MblFn )
mbfi1flim.2 
|- ( ph -> F : A --> RR )
Assertion mbfi1flim 
|- ( ph -> E. g ( g : NN --> dom S.1 /\ A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 mbfi1flim.1 
 |-  ( ph -> F e. MblFn )
2 mbfi1flim.2 
 |-  ( ph -> F : A --> RR )
3 iftrue 
 |-  ( y e. A -> if ( y e. A , ( F ` y ) , 0 ) = ( F ` y ) )
4 3 mpteq2ia 
 |-  ( y e. A |-> if ( y e. A , ( F ` y ) , 0 ) ) = ( y e. A |-> ( F ` y ) )
5 2 feqmptd 
 |-  ( ph -> F = ( y e. A |-> ( F ` y ) ) )
6 5 1 eqeltrrd 
 |-  ( ph -> ( y e. A |-> ( F ` y ) ) e. MblFn )
7 4 6 eqeltrid 
 |-  ( ph -> ( y e. A |-> if ( y e. A , ( F ` y ) , 0 ) ) e. MblFn )
8 fvex 
 |-  ( F ` y ) e. _V
9 c0ex 
 |-  0 e. _V
10 8 9 ifex 
 |-  if ( y e. A , ( F ` y ) , 0 ) e. _V
11 10 a1i 
 |-  ( ( ph /\ y e. A ) -> if ( y e. A , ( F ` y ) , 0 ) e. _V )
12 7 11 mbfdm2 
 |-  ( ph -> A e. dom vol )
13 mblss 
 |-  ( A e. dom vol -> A C_ RR )
14 12 13 syl 
 |-  ( ph -> A C_ RR )
15 rembl 
 |-  RR e. dom vol
16 15 a1i 
 |-  ( ph -> RR e. dom vol )
17 eldifn 
 |-  ( y e. ( RR \ A ) -> -. y e. A )
18 17 adantl 
 |-  ( ( ph /\ y e. ( RR \ A ) ) -> -. y e. A )
19 18 iffalsed 
 |-  ( ( ph /\ y e. ( RR \ A ) ) -> if ( y e. A , ( F ` y ) , 0 ) = 0 )
20 14 16 11 19 7 mbfss 
 |-  ( ph -> ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) e. MblFn )
21 2 ffvelcdmda 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. RR )
22 0red 
 |-  ( ( ph /\ -. y e. A ) -> 0 e. RR )
23 21 22 ifclda 
 |-  ( ph -> if ( y e. A , ( F ` y ) , 0 ) e. RR )
24 23 adantr 
 |-  ( ( ph /\ y e. RR ) -> if ( y e. A , ( F ` y ) , 0 ) e. RR )
25 24 fmpttd 
 |-  ( ph -> ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) : RR --> RR )
26 20 25 mbfi1flimlem 
 |-  ( ph -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) ) )
27 ssralv 
 |-  ( A C_ RR -> ( A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) -> A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) ) )
28 14 27 syl 
 |-  ( ph -> ( A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) -> A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) ) )
29 14 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
30 eleq1w 
 |-  ( y = x -> ( y e. A <-> x e. A ) )
31 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
32 30 31 ifbieq1d 
 |-  ( y = x -> if ( y e. A , ( F ` y ) , 0 ) = if ( x e. A , ( F ` x ) , 0 ) )
33 eqid 
 |-  ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) = ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) )
34 fvex 
 |-  ( F ` x ) e. _V
35 34 9 ifex 
 |-  if ( x e. A , ( F ` x ) , 0 ) e. _V
36 32 33 35 fvmpt 
 |-  ( x e. RR -> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) = if ( x e. A , ( F ` x ) , 0 ) )
37 29 36 syl 
 |-  ( ( ph /\ x e. A ) -> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) = if ( x e. A , ( F ` x ) , 0 ) )
38 iftrue 
 |-  ( x e. A -> if ( x e. A , ( F ` x ) , 0 ) = ( F ` x ) )
39 38 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( F ` x ) , 0 ) = ( F ` x ) )
40 37 39 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) = ( F ` x ) )
41 40 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) <-> ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )
42 41 ralbidva 
 |-  ( ph -> ( A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) <-> A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )
43 28 42 sylibd 
 |-  ( ph -> ( A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) -> A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )
44 43 anim2d 
 |-  ( ph -> ( ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) ) -> ( g : NN --> dom S.1 /\ A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
45 44 eximdv 
 |-  ( ph -> ( E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( ( y e. RR |-> if ( y e. A , ( F ` y ) , 0 ) ) ` x ) ) -> E. g ( g : NN --> dom S.1 /\ A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) ) )
46 26 45 mpd 
 |-  ( ph -> E. g ( g : NN --> dom S.1 /\ A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )