Metamath Proof Explorer

Theorem mbfresmf

Description: A real-valued measurable function is a sigma-measurable function (w.r.t. the Lebesgue measure on the Reals). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses mbfresmf.1 
|- ( ph -> F e. MblFn )
mbfresmf.2 
|- ( ph -> ran F C_ RR )
mbfresmf.3 
|- S = dom vol
Assertion mbfresmf 
|- ( ph -> F e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 mbfresmf.1 
 |-  ( ph -> F e. MblFn )
2 mbfresmf.2 
 |-  ( ph -> ran F C_ RR )
3 mbfresmf.3 
 |-  S = dom vol
4 nfv 
 |-  F/ a ph
5 3 a1i 
 |-  ( ph -> S = dom vol )
6 dmvolsal 
 |-  dom vol e. SAlg
7 6 a1i 
 |-  ( ph -> dom vol e. SAlg )
8 5 7 eqeltrd 
 |-  ( ph -> S e. SAlg )
9 mbfdmssre 
 |-  ( F e. MblFn -> dom F C_ RR )
10 1 9 syl 
 |-  ( ph -> dom F C_ RR )
11 3 unieqi 
 |-  U. S = U. dom vol
12 unidmvol 
 |-  U. dom vol = RR
13 11 12 eqtri 
 |-  U. S = RR
14 10 13 sseqtrrdi 
 |-  ( ph -> dom F C_ U. S )
15 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
16 ffn 
 |-  ( F : dom F --> CC -> F Fn dom F )
17 1 15 16 3syl 
 |-  ( ph -> F Fn dom F )
18 17 2 jca 
 |-  ( ph -> ( F Fn dom F /\ ran F C_ RR ) )
19 df-f 
 |-  ( F : dom F --> RR <-> ( F Fn dom F /\ ran F C_ RR ) )
20 18 19 sylibr 
 |-  ( ph -> F : dom F --> RR )
21 20 adantr 
 |-  ( ( ph /\ a e. RR ) -> F : dom F --> RR )
22 rexr 
 |-  ( a e. RR -> a e. RR* )
23 22 adantl 
 |-  ( ( ph /\ a e. RR ) -> a e. RR* )
24 21 23 preimaioomnf 
 |-  ( ( ph /\ a e. RR ) -> ( `' F " ( -oo (,) a ) ) = { x e. dom F | ( F ` x ) < a } )
25 24 eqcomd 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } = ( `' F " ( -oo (,) a ) ) )
26 6 elexi 
 |-  dom vol e. _V
27 3 26 eqeltri 
 |-  S e. _V
28 27 a1i 
 |-  ( ( ph /\ a e. RR ) -> S e. _V )
29 1 dmexd 
 |-  ( ph -> dom F e. _V )
30 29 adantr 
 |-  ( ( ph /\ a e. RR ) -> dom F e. _V )
31 mbfima 
 |-  ( ( F e. MblFn /\ F : dom F --> RR ) -> ( `' F " ( -oo (,) a ) ) e. dom vol )
32 1 20 31 syl2anc 
 |-  ( ph -> ( `' F " ( -oo (,) a ) ) e. dom vol )
33 32 5 eleqtrrd 
 |-  ( ph -> ( `' F " ( -oo (,) a ) ) e. S )
34 33 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( `' F " ( -oo (,) a ) ) e. S )
35 cnvimass 
 |-  ( `' F " ( -oo (,) a ) ) C_ dom F
36 dfss 
 |-  ( ( `' F " ( -oo (,) a ) ) C_ dom F <-> ( `' F " ( -oo (,) a ) ) = ( ( `' F " ( -oo (,) a ) ) i^i dom F ) )
37 36 biimpi 
 |-  ( ( `' F " ( -oo (,) a ) ) C_ dom F -> ( `' F " ( -oo (,) a ) ) = ( ( `' F " ( -oo (,) a ) ) i^i dom F ) )
38 35 37 ax-mp 
 |-  ( `' F " ( -oo (,) a ) ) = ( ( `' F " ( -oo (,) a ) ) i^i dom F )
39 28 30 34 38 elrestd 
 |-  ( ( ph /\ a e. RR ) -> ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
40 25 39 eqeltrd 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) )
41 4 8 14 20 40 issmfd 
 |-  ( ph -> F e. ( SMblFn ` S ) )