# Metamath Proof Explorer

## Theorem ismbfm

Description: The predicate " F is a measurable function from the measurable space S to the measurable space T ". Cf. ismbf . (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Hypotheses ismbfm.1
`|- ( ph -> S e. U. ran sigAlgebra )`
ismbfm.2
`|- ( ph -> T e. U. ran sigAlgebra )`
Assertion ismbfm
`|- ( ph -> ( F e. ( S MblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) ) )`

### Proof

Step Hyp Ref Expression
1 ismbfm.1
` |-  ( ph -> S e. U. ran sigAlgebra )`
2 ismbfm.2
` |-  ( ph -> T e. U. ran sigAlgebra )`
3 unieq
` |-  ( s = S -> U. s = U. S )`
4 3 oveq2d
` |-  ( s = S -> ( U. t ^m U. s ) = ( U. t ^m U. S ) )`
5 eleq2
` |-  ( s = S -> ( ( `' f " x ) e. s <-> ( `' f " x ) e. S ) )`
6 5 ralbidv
` |-  ( s = S -> ( A. x e. t ( `' f " x ) e. s <-> A. x e. t ( `' f " x ) e. S ) )`
7 4 6 rabeqbidv
` |-  ( s = S -> { f e. ( U. t ^m U. s ) | A. x e. t ( `' f " x ) e. s } = { f e. ( U. t ^m U. S ) | A. x e. t ( `' f " x ) e. S } )`
8 unieq
` |-  ( t = T -> U. t = U. T )`
9 8 oveq1d
` |-  ( t = T -> ( U. t ^m U. S ) = ( U. T ^m U. S ) )`
10 raleq
` |-  ( t = T -> ( A. x e. t ( `' f " x ) e. S <-> A. x e. T ( `' f " x ) e. S ) )`
11 9 10 rabeqbidv
` |-  ( t = T -> { f e. ( U. t ^m U. S ) | A. x e. t ( `' f " x ) e. S } = { f e. ( U. T ^m U. S ) | A. x e. T ( `' f " x ) e. S } )`
12 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 } )`
13 ovex
` |-  ( U. T ^m U. S ) e. _V`
14 13 rabex
` |-  { f e. ( U. T ^m U. S ) | A. x e. T ( `' f " x ) e. S } e. _V`
15 7 11 12 14 ovmpo
` |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S MblFnM T ) = { f e. ( U. T ^m U. S ) | A. x e. T ( `' f " x ) e. S } )`
16 1 2 15 syl2anc
` |-  ( ph -> ( S MblFnM T ) = { f e. ( U. T ^m U. S ) | A. x e. T ( `' f " x ) e. S } )`
17 16 eleq2d
` |-  ( ph -> ( F e. ( S MblFnM T ) <-> F e. { f e. ( U. T ^m U. S ) | A. x e. T ( `' f " x ) e. S } ) )`
18 cnveq
` |-  ( f = F -> `' f = `' F )`
19 18 imaeq1d
` |-  ( f = F -> ( `' f " x ) = ( `' F " x ) )`
20 19 eleq1d
` |-  ( f = F -> ( ( `' f " x ) e. S <-> ( `' F " x ) e. S ) )`
21 20 ralbidv
` |-  ( f = F -> ( A. x e. T ( `' f " x ) e. S <-> A. x e. T ( `' F " x ) e. S ) )`
22 21 elrab
` |-  ( F e. { f e. ( U. T ^m U. S ) | A. x e. T ( `' f " x ) e. S } <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) )`
23 17 22 syl6bb
` |-  ( ph -> ( F e. ( S MblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) ) )`