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 bitrdi 
 |-  ( ph -> ( F e. ( S MblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) ) )