Theorem cnmbfm

Description: A continuous function is measurable with respect to the Borel Algebra of its domain and range. (Contributed by Thierry Arnoux, 3-Jun-2017)

	Ref	Expression
Hypotheses	cnmbfm.1	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
	cnmbfm.2	$$⊢\phi \to S=𝛔\left(J\right)$$
	cnmbfm.3	$$⊢\phi \to T=𝛔\left(K\right)$$
Assertion	cnmbfm	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmbfm.1	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
2		cnmbfm.2	$$⊢\phi \to S=𝛔\left(J\right)$$
3		cnmbfm.3	$$⊢\phi \to T=𝛔\left(K\right)$$
4		eqid	$$⊢\bigcup J=\bigcup J$$
5		eqid	$$⊢\bigcup K=\bigcup K$$
6	4 5	cnf	$$⊢F\in \left(J\mathrm{Cn}K\right)\to F:\bigcup J⟶\bigcup K$$
7	1 6	syl	$$⊢\phi \to F:\bigcup J⟶\bigcup K$$
8	2	unieqd	$$⊢\phi \to \bigcup S=\bigcup 𝛔\left(J\right)$$
9		cntop1	$$⊢F\in \left(J\mathrm{Cn}K\right)\to J\in \mathrm{Top}$$
10		unisg	$$⊢J\in \mathrm{Top}\to \bigcup 𝛔\left(J\right)=\bigcup J$$
11	1 9 10	3syl	$$⊢\phi \to \bigcup 𝛔\left(J\right)=\bigcup J$$
12	8 11	eqtrd	$$⊢\phi \to \bigcup S=\bigcup J$$
13	3	unieqd	$$⊢\phi \to \bigcup T=\bigcup 𝛔\left(K\right)$$
14		cntop2	$$⊢F\in \left(J\mathrm{Cn}K\right)\to K\in \mathrm{Top}$$
15		unisg	$$⊢K\in \mathrm{Top}\to \bigcup 𝛔\left(K\right)=\bigcup K$$
16	1 14 15	3syl	$$⊢\phi \to \bigcup 𝛔\left(K\right)=\bigcup K$$
17	13 16	eqtrd	$$⊢\phi \to \bigcup T=\bigcup K$$
18	12 17	feq23d	$$⊢\phi \to \left(F:\bigcup S⟶\bigcup T\leftrightarrow F:\bigcup J⟶\bigcup K\right)$$
19	7 18	mpbird	$$⊢\phi \to F:\bigcup S⟶\bigcup T$$
20		sssigagen	$$⊢J\in \mathrm{Top}\to J\subseteq 𝛔\left(J\right)$$
21	1 9 20	3syl	$$⊢\phi \to J\subseteq 𝛔\left(J\right)$$
22	21 2	sseqtrrd	$$⊢\phi \to J\subseteq S$$
23	22	adantr	$$⊢\left(\phi \wedge a\in K\right)\to J\subseteq S$$
24		cnima	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge a\in K\right)\to F^{-1}\left[a\right]\in J$$
25	1 24	sylan	$$⊢\left(\phi \wedge a\in K\right)\to F^{-1}\left[a\right]\in J$$
26	23 25	sseldd	$$⊢\left(\phi \wedge a\in K\right)\to F^{-1}\left[a\right]\in S$$
27	26	ralrimiva	$$⊢\phi \to \forall a\in K{F}^{-1}\left[a\right]\in S$$
28		elex	$$⊢K\in \mathrm{Top}\to K\in \mathrm{V}$$
29	1 14 28	3syl	$$⊢\phi \to K\in \mathrm{V}$$
30		sigagensiga	$$⊢J\in \mathrm{Top}\to 𝛔\left(J\right)\in \mathrm{sigAlgebra}\left(\bigcup J\right)$$
31	1 9 30	3syl	$$⊢\phi \to 𝛔\left(J\right)\in \mathrm{sigAlgebra}\left(\bigcup J\right)$$
32	2 31	eqeltrd	$$⊢\phi \to S\in \mathrm{sigAlgebra}\left(\bigcup J\right)$$
33		elrnsiga	$$⊢S\in \mathrm{sigAlgebra}\left(\bigcup J\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
34	32 33	syl	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
35	29 34 3	imambfm	$$⊢\phi \to \left(F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\leftrightarrow \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)$$
36	19 27 35	mpbir2and	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$