Metamath Proof Explorer

Theorem mbfpsssmf

Description: Real-valued measurable functions are a proper subset of sigma-measurable functions (w.r.t. the Lebesgue measure on the reals). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis mbfpsssmf.1 
|- S = dom vol
Assertion mbfpsssmf 
|- ( MblFn i^i ( RR ^pm RR ) ) C. ( SMblFn ` S )

Proof

Step Hyp Ref Expression
1 mbfpsssmf.1 
 |-  S = dom vol
2 elinel1 
 |-  ( f e. ( MblFn i^i ( RR ^pm RR ) ) -> f e. MblFn )
3 elinel2 
 |-  ( f e. ( MblFn i^i ( RR ^pm RR ) ) -> f e. ( RR ^pm RR ) )
4 elpmrn 
 |-  ( f e. ( RR ^pm RR ) -> ran f C_ RR )
5 3 4 syl 
 |-  ( f e. ( MblFn i^i ( RR ^pm RR ) ) -> ran f C_ RR )
6 2 5 1 mbfresmf 
 |-  ( f e. ( MblFn i^i ( RR ^pm RR ) ) -> f e. ( SMblFn ` S ) )
7 6 ssriv 
 |-  ( MblFn i^i ( RR ^pm RR ) ) C_ ( SMblFn ` S )
8 1 nsssmfmbf 
 |-  -. ( SMblFn ` S ) C_ MblFn
9 2 ssriv 
 |-  ( MblFn i^i ( RR ^pm RR ) ) C_ MblFn
10 nsstr 
 |-  ( ( -. ( SMblFn ` S ) C_ MblFn /\ ( MblFn i^i ( RR ^pm RR ) ) C_ MblFn ) -> -. ( SMblFn ` S ) C_ ( MblFn i^i ( RR ^pm RR ) ) )
11 8 9 10 mp2an 
 |-  -. ( SMblFn ` S ) C_ ( MblFn i^i ( RR ^pm RR ) )
12 7 11 pm3.2i 
 |-  ( ( MblFn i^i ( RR ^pm RR ) ) C_ ( SMblFn ` S ) /\ -. ( SMblFn ` S ) C_ ( MblFn i^i ( RR ^pm RR ) ) )
13 dfpss3 
 |-  ( ( MblFn i^i ( RR ^pm RR ) ) C. ( SMblFn ` S ) <-> ( ( MblFn i^i ( RR ^pm RR ) ) C_ ( SMblFn ` S ) /\ -. ( SMblFn ` S ) C_ ( MblFn i^i ( RR ^pm RR ) ) ) )
14 12 13 mpbir 
 |-  ( MblFn i^i ( RR ^pm RR ) ) C. ( SMblFn ` S )