# Metamath Proof Explorer

## 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}↔{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}\phantom{\rule{.4em}{0ex}}{{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)↔\left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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)$