Metamath Proof Explorer

Theorem mbfmcnt

Description: All functions are measurable with respect to the counting measure. (Contributed by Thierry Arnoux, 24-Jan-2017)

Ref Expression
Assertion mbfmcnt 
|- ( O e. V -> ( ~P O MblFnM BrSiga ) = ( RR ^m O ) )

Proof

Step Hyp Ref Expression
1 pwsiga 
 |-  ( O e. V -> ~P O e. ( sigAlgebra ` O ) )
2 elrnsiga 
 |-  ( ~P O e. ( sigAlgebra ` O ) -> ~P O e. U. ran sigAlgebra )
3 1 2 syl 
 |-  ( O e. V -> ~P O e. U. ran sigAlgebra )
4 brsigarn 
 |-  BrSiga e. ( sigAlgebra ` RR )
5 elrnsiga 
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
6 4 5 mp1i 
 |-  ( O e. V -> BrSiga e. U. ran sigAlgebra )
7 3 6 ismbfm 
 |-  ( O e. V -> ( f e. ( ~P O MblFnM BrSiga ) <-> ( f e. ( U. BrSiga ^m U. ~P O ) /\ A. x e. BrSiga ( `' f " x ) e. ~P O ) ) )
8 unibrsiga 
 |-  U. BrSiga = RR
9 reex 
 |-  RR e. _V
10 8 9 eqeltri 
 |-  U. BrSiga e. _V
11 unipw 
 |-  U. ~P O = O
12 elex 
 |-  ( O e. V -> O e. _V )
13 11 12 eqeltrid 
 |-  ( O e. V -> U. ~P O e. _V )
14 elmapg 
 |-  ( ( U. BrSiga e. _V /\ U. ~P O e. _V ) -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : U. ~P O --> U. BrSiga ) )
15 10 13 14 sylancr 
 |-  ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : U. ~P O --> U. BrSiga ) )
16 11 feq2i 
 |-  ( f : U. ~P O --> U. BrSiga <-> f : O --> U. BrSiga )
17 15 16 syl6bb 
 |-  ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : O --> U. BrSiga ) )
18 ffn 
 |-  ( f : O --> U. BrSiga -> f Fn O )
19 17 18 syl6bi 
 |-  ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) -> f Fn O ) )
20 elpreima 
 |-  ( f Fn O -> ( y e. ( `' f " x ) <-> ( y e. O /\ ( f ` y ) e. x ) ) )
21 simpl 
 |-  ( ( y e. O /\ ( f ` y ) e. x ) -> y e. O )
22 20 21 syl6bi 
 |-  ( f Fn O -> ( y e. ( `' f " x ) -> y e. O ) )
23 22 ssrdv 
 |-  ( f Fn O -> ( `' f " x ) C_ O )
24 vex 
 |-  f e. _V
25 24 cnvex 
 |-  `' f e. _V
26 imaexg 
 |-  ( `' f e. _V -> ( `' f " x ) e. _V )
27 25 26 ax-mp 
 |-  ( `' f " x ) e. _V
28 27 elpw 
 |-  ( ( `' f " x ) e. ~P O <-> ( `' f " x ) C_ O )
29 23 28 sylibr 
 |-  ( f Fn O -> ( `' f " x ) e. ~P O )
30 29 ralrimivw 
 |-  ( f Fn O -> A. x e. BrSiga ( `' f " x ) e. ~P O )
31 19 30 syl6 
 |-  ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) -> A. x e. BrSiga ( `' f " x ) e. ~P O ) )
32 31 pm4.71d 
 |-  ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> ( f e. ( U. BrSiga ^m U. ~P O ) /\ A. x e. BrSiga ( `' f " x ) e. ~P O ) ) )
33 7 32 bitr4d 
 |-  ( O e. V -> ( f e. ( ~P O MblFnM BrSiga ) <-> f e. ( U. BrSiga ^m U. ~P O ) ) )
34 33 eqrdv 
 |-  ( O e. V -> ( ~P O MblFnM BrSiga ) = ( U. BrSiga ^m U. ~P O ) )
35 8 11 oveq12i 
 |-  ( U. BrSiga ^m U. ~P O ) = ( RR ^m O )
36 34 35 eqtrdi 
 |-  ( O e. V -> ( ~P O MblFnM BrSiga ) = ( RR ^m O ) )