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 syl6eqr
 |-  ( 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 ) )