Metamath Proof Explorer

Theorem elunirnmbfm

Description: The property of being a measurable function. (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Assertion elunirnmbfm 
|- ( F e. U. ran MblFnM <-> E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) )

Proof

Step Hyp Ref Expression
1 df-mbfm 
 |-  MblFnM = ( s e. U. ran sigAlgebra , t e. U. ran sigAlgebra |-> { f e. ( U. t ^m U. s ) | A. x e. t ( `' f " x ) e. s } )
2 1 mpofun 
 |-  Fun MblFnM
3 elunirn 
 |-  ( Fun MblFnM -> ( F e. U. ran MblFnM <-> E. a e. dom MblFnM F e. ( MblFnM ` a ) ) )
4 2 3 ax-mp 
 |-  ( F e. U. ran MblFnM <-> E. a e. dom MblFnM F e. ( MblFnM ` a ) )
5 ovex 
 |-  ( U. t ^m U. s ) e. _V
6 5 rabex 
 |-  { f e. ( U. t ^m U. s ) | A. x e. t ( `' f " x ) e. s } e. _V
7 1 6 dmmpo 
 |-  dom MblFnM = ( U. ran sigAlgebra X. U. ran sigAlgebra )
8 7 rexeqi 
 |-  ( E. a e. dom MblFnM F e. ( MblFnM ` a ) <-> E. a e. ( U. ran sigAlgebra X. U. ran sigAlgebra ) F e. ( MblFnM ` a ) )
9 fveq2 
 |-  ( a = <. s , t >. -> ( MblFnM ` a ) = ( MblFnM ` <. s , t >. ) )
10 df-ov 
 |-  ( s MblFnM t ) = ( MblFnM ` <. s , t >. )
11 9 10 eqtr4di 
 |-  ( a = <. s , t >. -> ( MblFnM ` a ) = ( s MblFnM t ) )
12 11 eleq2d 
 |-  ( a = <. s , t >. -> ( F e. ( MblFnM ` a ) <-> F e. ( s MblFnM t ) ) )
13 12 rexxp 
 |-  ( E. a e. ( U. ran sigAlgebra X. U. ran sigAlgebra ) F e. ( MblFnM ` a ) <-> E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra F e. ( s MblFnM t ) )
14 4 8 13 3bitri 
 |-  ( F e. U. ran MblFnM <-> E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra F e. ( s MblFnM t ) )
15 simpl 
 |-  ( ( s e. U. ran sigAlgebra /\ t e. U. ran sigAlgebra ) -> s e. U. ran sigAlgebra )
16 simpr 
 |-  ( ( s e. U. ran sigAlgebra /\ t e. U. ran sigAlgebra ) -> t e. U. ran sigAlgebra )
17 15 16 ismbfm 
 |-  ( ( s e. U. ran sigAlgebra /\ t e. U. ran sigAlgebra ) -> ( F e. ( s MblFnM t ) <-> ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) ) )
18 17 2rexbiia 
 |-  ( E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra F e. ( s MblFnM t ) <-> E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) )
19 14 18 bitri 
 |-  ( F e. U. ran MblFnM <-> E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) )