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)\leftrightarrow \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{\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)\leftrightarrow \left(G\circ F\in \left({\bigcup T}^{\bigcup R}\right)\wedge \forall a\in T{\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)$$