Metamath Proof Explorer

Theorem isanmbfm

Description: The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Hypotheses mbfmf.1 
|- ( ph -> S e. U. ran sigAlgebra )
mbfmf.2 
|- ( ph -> T e. U. ran sigAlgebra )
mbfmf.3 
|- ( ph -> F e. ( S MblFnM T ) )
Assertion isanmbfm 
|- ( ph -> F e. U. ran MblFnM )

Proof

Step Hyp Ref Expression
1 mbfmf.1 
 |-  ( ph -> S e. U. ran sigAlgebra )
2 mbfmf.2 
 |-  ( ph -> T e. U. ran sigAlgebra )
3 mbfmf.3 
 |-  ( ph -> F e. ( S MblFnM T ) )
4 1 2 ismbfm 
 |-  ( ph -> ( F e. ( S MblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) ) )
5 3 4 mpbid 
 |-  ( ph -> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) )
6 unieq 
 |-  ( s = S -> U. s = U. S )
7 6 oveq2d 
 |-  ( s = S -> ( U. t ^m U. s ) = ( U. t ^m U. S ) )
8 7 eleq2d 
 |-  ( s = S -> ( F e. ( U. t ^m U. s ) <-> F e. ( U. t ^m U. S ) ) )
9 eleq2 
 |-  ( s = S -> ( ( `' F " x ) e. s <-> ( `' F " x ) e. S ) )
10 9 ralbidv 
 |-  ( s = S -> ( A. x e. t ( `' F " x ) e. s <-> A. x e. t ( `' F " x ) e. S ) )
11 8 10 anbi12d 
 |-  ( 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 ) ) )
12 unieq 
 |-  ( t = T -> U. t = U. T )
13 12 oveq1d 
 |-  ( t = T -> ( U. t ^m U. S ) = ( U. T ^m U. S ) )
14 13 eleq2d 
 |-  ( t = T -> ( F e. ( U. t ^m U. S ) <-> F e. ( U. T ^m U. S ) ) )
15 raleq 
 |-  ( t = T -> ( A. x e. t ( `' F " x ) e. S <-> A. x e. T ( `' F " x ) e. S ) )
16 14 15 anbi12d 
 |-  ( 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 ) ) )
17 11 16 rspc2ev 
 |-  ( ( 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 ) ) -> 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 ) )
18 1 2 5 17 syl3anc 
 |-  ( ph -> 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 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 ) )
20 18 19 sylibr 
 |-  ( ph -> F e. U. ran MblFnM )