# 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 ${⊢}{\phi }\to {R}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
mbfmco.2 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
mbfmco.3 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
mbfmco.4 ${⊢}{\phi }\to {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{S}\right)$
mbfmco.5 ${⊢}{\phi }\to {G}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)$
Assertion mbfmco ${⊢}{\phi }\to {G}\circ {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{T}\right)$

### Proof

Step Hyp Ref Expression
1 mbfmco.1 ${⊢}{\phi }\to {R}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
2 mbfmco.2 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 mbfmco.3 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
4 mbfmco.4 ${⊢}{\phi }\to {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{S}\right)$
5 mbfmco.5 ${⊢}{\phi }\to {G}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)$
6 2 3 5 mbfmf ${⊢}{\phi }\to {G}:\bigcup {S}⟶\bigcup {T}$
7 1 2 4 mbfmf ${⊢}{\phi }\to {F}:\bigcup {R}⟶\bigcup {S}$
8 fco ${⊢}\left({G}:\bigcup {S}⟶\bigcup {T}\wedge {F}:\bigcup {R}⟶\bigcup {S}\right)\to \left({G}\circ {F}\right):\bigcup {R}⟶\bigcup {T}$
9 6 7 8 syl2anc ${⊢}{\phi }\to \left({G}\circ {F}\right):\bigcup {R}⟶\bigcup {T}$
10 unielsiga ${⊢}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup {T}\in {T}$
11 3 10 syl ${⊢}{\phi }\to \bigcup {T}\in {T}$
12 unielsiga ${⊢}{R}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup {R}\in {R}$
13 1 12 syl ${⊢}{\phi }\to \bigcup {R}\in {R}$
14 11 13 elmapd ${⊢}{\phi }\to \left({G}\circ {F}\in \left({\bigcup {T}}^{\bigcup {R}}\right)↔\left({G}\circ {F}\right):\bigcup {R}⟶\bigcup {T}\right)$
15 9 14 mpbird ${⊢}{\phi }\to {G}\circ {F}\in \left({\bigcup {T}}^{\bigcup {R}}\right)$
16 cnvco ${⊢}{\left({G}\circ {F}\right)}^{-1}={{F}}^{-1}\circ {{G}}^{-1}$
17 16 imaeq1i ${⊢}{\left({G}\circ {F}\right)}^{-1}\left[{a}\right]=\left({{F}}^{-1}\circ {{G}}^{-1}\right)\left[{a}\right]$
18 imaco ${⊢}\left({{F}}^{-1}\circ {{G}}^{-1}\right)\left[{a}\right]={{F}}^{-1}\left[{{G}}^{-1}\left[{a}\right]\right]$
19 17 18 eqtri ${⊢}{\left({G}\circ {F}\right)}^{-1}\left[{a}\right]={{F}}^{-1}\left[{{G}}^{-1}\left[{a}\right]\right]$
20 1 adantr ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {R}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
21 2 adantr ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
22 4 adantr ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{S}\right)$
23 3 adantr ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
24 5 adantr ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {G}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)$
25 simpr ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {a}\in {T}$
26 21 23 24 25 mbfmcnvima ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {{G}}^{-1}\left[{a}\right]\in {S}$
27 20 21 22 26 mbfmcnvima ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {{F}}^{-1}\left[{{G}}^{-1}\left[{a}\right]\right]\in {R}$
28 19 27 eqeltrid ${⊢}\left({\phi }\wedge {a}\in {T}\right)\to {\left({G}\circ {F}\right)}^{-1}\left[{a}\right]\in {R}$
29 28 ralrimiva ${⊢}{\phi }\to \forall {a}\in {T}\phantom{\rule{.4em}{0ex}}{\left({G}\circ {F}\right)}^{-1}\left[{a}\right]\in {R}$
30 1 3 ismbfm ${⊢}{\phi }\to \left({G}\circ {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{T}\right)↔\left({G}\circ {F}\in \left({\bigcup {T}}^{\bigcup {R}}\right)\wedge \forall {a}\in {T}\phantom{\rule{.4em}{0ex}}{\left({G}\circ {F}\right)}^{-1}\left[{a}\right]\in {R}\right)\right)$
31 15 29 30 mpbir2and ${⊢}{\phi }\to {G}\circ {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{T}\right)$