# 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 ) )`