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