Metamath Proof Explorer

Theorem mbfmco

Description: The composition of two measurable functions is measurable. See cnmpt11 . (Contributed by Thierry Arnoux, 4-Jun-2017)

Ref Expression
Hypotheses mbfmco.1 
|- ( ph -> R e. U. ran sigAlgebra )
mbfmco.2 
|- ( ph -> S e. U. ran sigAlgebra )
mbfmco.3 
|- ( ph -> T e. U. ran sigAlgebra )
mbfmco.4 
|- ( ph -> F e. ( R MblFnM S ) )
mbfmco.5 
|- ( ph -> G e. ( S MblFnM T ) )
Assertion mbfmco 
|- ( ph -> ( G o. F ) e. ( R MblFnM T ) )

Proof

Step Hyp Ref Expression
1 mbfmco.1 
 |-  ( ph -> R e. U. ran sigAlgebra )
2 mbfmco.2 
 |-  ( ph -> S e. U. ran sigAlgebra )
3 mbfmco.3 
 |-  ( ph -> T e. U. ran sigAlgebra )
4 mbfmco.4 
 |-  ( ph -> F e. ( R MblFnM S ) )
5 mbfmco.5 
 |-  ( ph -> G e. ( S MblFnM T ) )
6 2 3 5 mbfmf 
 |-  ( ph -> G : U. S --> U. T )
7 1 2 4 mbfmf 
 |-  ( ph -> F : U. R --> U. S )
8 fco 
 |-  ( ( G : U. S --> U. T /\ F : U. R --> U. S ) -> ( G o. F ) : U. R --> U. T )
9 6 7 8 syl2anc 
 |-  ( ph -> ( G o. F ) : U. R --> U. T )
10 unielsiga 
 |-  ( T e. U. ran sigAlgebra -> U. T e. T )
11 3 10 syl 
 |-  ( ph -> U. T e. T )
12 unielsiga 
 |-  ( R e. U. ran sigAlgebra -> U. R e. R )
13 1 12 syl 
 |-  ( ph -> U. R e. R )
14 11 13 elmapd 
 |-  ( ph -> ( ( G o. F ) e. ( U. T ^m U. R ) <-> ( G o. F ) : U. R --> U. T ) )
15 9 14 mpbird 
 |-  ( ph -> ( G o. F ) e. ( U. T ^m U. R ) )
16 cnvco 
 |-  `' ( G o. F ) = ( `' F o. `' G )
17 16 imaeq1i 
 |-  ( `' ( G o. F ) " a ) = ( ( `' F o. `' G ) " a )
18 imaco 
 |-  ( ( `' F o. `' G ) " a ) = ( `' F " ( `' G " a ) )
19 17 18 eqtri 
 |-  ( `' ( G o. F ) " a ) = ( `' F " ( `' G " a ) )
20 1 adantr 
 |-  ( ( ph /\ a e. T ) -> R e. U. ran sigAlgebra )
21 2 adantr 
 |-  ( ( ph /\ a e. T ) -> S e. U. ran sigAlgebra )
22 4 adantr 
 |-  ( ( ph /\ a e. T ) -> F e. ( R MblFnM S ) )
23 3 adantr 
 |-  ( ( ph /\ a e. T ) -> T e. U. ran sigAlgebra )
24 5 adantr 
 |-  ( ( ph /\ a e. T ) -> G e. ( S MblFnM T ) )
25 simpr 
 |-  ( ( ph /\ a e. T ) -> a e. T )
26 21 23 24 25 mbfmcnvima 
 |-  ( ( ph /\ a e. T ) -> ( `' G " a ) e. S )
27 20 21 22 26 mbfmcnvima 
 |-  ( ( ph /\ a e. T ) -> ( `' F " ( `' G " a ) ) e. R )
28 19 27 eqeltrid 
 |-  ( ( ph /\ a e. T ) -> ( `' ( G o. F ) " a ) e. R )
29 28 ralrimiva 
 |-  ( ph -> A. a e. T ( `' ( G o. F ) " a ) e. R )
30 1 3 ismbfm 
 |-  ( ph -> ( ( G o. F ) e. ( R MblFnM T ) <-> ( ( G o. F ) e. ( U. T ^m U. R ) /\ A. a e. T ( `' ( G o. F ) " a ) e. R ) ) )
31 15 29 30 mpbir2and 
 |-  ( ph -> ( G o. F ) e. ( R MblFnM T ) )