# Metamath Proof Explorer

## Theorem mbfmco2

Description: The pair building of two measurable functions is measurable. ( cf. cnmpt1t ). (Contributed by Thierry Arnoux, 6-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}$
mbfmco2.4 ${⊢}{\phi }\to {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{S}\right)$
mbfmco2.5 ${⊢}{\phi }\to {G}\in \left({R}{\mathrm{MblFn}}_{\mu }{T}\right)$
mbfmco2.6 ${⊢}{H}=\left({x}\in \bigcup {R}⟼⟨{F}\left({x}\right),{G}\left({x}\right)⟩\right)$
Assertion mbfmco2 ${⊢}{\phi }\to {H}\in \left({R}{\mathrm{MblFn}}_{\mu }\left({S}{×}_{s}{T}\right)\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 mbfmco2.4 ${⊢}{\phi }\to {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{S}\right)$
5 mbfmco2.5 ${⊢}{\phi }\to {G}\in \left({R}{\mathrm{MblFn}}_{\mu }{T}\right)$
6 mbfmco2.6 ${⊢}{H}=\left({x}\in \bigcup {R}⟼⟨{F}\left({x}\right),{G}\left({x}\right)⟩\right)$
7 1 2 4 mbfmf ${⊢}{\phi }\to {F}:\bigcup {R}⟶\bigcup {S}$
8 7 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in \bigcup {R}\right)\to {F}\left({x}\right)\in \bigcup {S}$
9 1 3 5 mbfmf ${⊢}{\phi }\to {G}:\bigcup {R}⟶\bigcup {T}$
10 9 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in \bigcup {R}\right)\to {G}\left({x}\right)\in \bigcup {T}$
11 opelxpi ${⊢}\left({F}\left({x}\right)\in \bigcup {S}\wedge {G}\left({x}\right)\in \bigcup {T}\right)\to ⟨{F}\left({x}\right),{G}\left({x}\right)⟩\in \left(\bigcup {S}×\bigcup {T}\right)$
12 8 10 11 syl2anc ${⊢}\left({\phi }\wedge {x}\in \bigcup {R}\right)\to ⟨{F}\left({x}\right),{G}\left({x}\right)⟩\in \left(\bigcup {S}×\bigcup {T}\right)$
13 sxuni ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to \bigcup {S}×\bigcup {T}=\bigcup \left({S}{×}_{s}{T}\right)$
14 2 3 13 syl2anc ${⊢}{\phi }\to \bigcup {S}×\bigcup {T}=\bigcup \left({S}{×}_{s}{T}\right)$
15 14 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcup {R}\right)\to \bigcup {S}×\bigcup {T}=\bigcup \left({S}{×}_{s}{T}\right)$
16 12 15 eleqtrd ${⊢}\left({\phi }\wedge {x}\in \bigcup {R}\right)\to ⟨{F}\left({x}\right),{G}\left({x}\right)⟩\in \bigcup \left({S}{×}_{s}{T}\right)$
17 16 6 fmptd ${⊢}{\phi }\to {H}:\bigcup {R}⟶\bigcup \left({S}{×}_{s}{T}\right)$
18 eqid ${⊢}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)=\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)$
19 vex ${⊢}{a}\in \mathrm{V}$
20 vex ${⊢}{b}\in \mathrm{V}$
21 19 20 xpex ${⊢}{a}×{b}\in \mathrm{V}$
22 18 21 elrnmpo ${⊢}{c}\in \mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)↔\exists {a}\in {S}\phantom{\rule{.4em}{0ex}}\exists {b}\in {T}\phantom{\rule{.4em}{0ex}}{c}={a}×{b}$
23 simp3 ${⊢}\left({\phi }\wedge \left({a}\in {S}\wedge {b}\in {T}\right)\wedge {c}={a}×{b}\right)\to {c}={a}×{b}$
24 23 imaeq2d ${⊢}\left({\phi }\wedge \left({a}\in {S}\wedge {b}\in {T}\right)\wedge {c}={a}×{b}\right)\to {{H}}^{-1}\left[{c}\right]={{H}}^{-1}\left[{a}×{b}\right]$
25 simp1 ${⊢}\left({\phi }\wedge \left({a}\in {S}\wedge {b}\in {T}\right)\wedge {c}={a}×{b}\right)\to {\phi }$
26 simp2l ${⊢}\left({\phi }\wedge \left({a}\in {S}\wedge {b}\in {T}\right)\wedge {c}={a}×{b}\right)\to {a}\in {S}$
27 simp2r ${⊢}\left({\phi }\wedge \left({a}\in {S}\wedge {b}\in {T}\right)\wedge {c}={a}×{b}\right)\to {b}\in {T}$
28 7 9 6 xppreima2 ${⊢}{\phi }\to {{H}}^{-1}\left[{a}×{b}\right]={{F}}^{-1}\left[{a}\right]\cap {{G}}^{-1}\left[{b}\right]$
29 28 3ad2ant1 ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {{H}}^{-1}\left[{a}×{b}\right]={{F}}^{-1}\left[{a}\right]\cap {{G}}^{-1}\left[{b}\right]$
30 1 3ad2ant1 ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {R}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
31 2 3ad2ant1 ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
32 4 3ad2ant1 ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {F}\in \left({R}{\mathrm{MblFn}}_{\mu }{S}\right)$
33 simp2 ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {a}\in {S}$
34 30 31 32 33 mbfmcnvima ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {{F}}^{-1}\left[{a}\right]\in {R}$
35 3 3ad2ant1 ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
36 5 3ad2ant1 ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {G}\in \left({R}{\mathrm{MblFn}}_{\mu }{T}\right)$
37 simp3 ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {b}\in {T}$
38 30 35 36 37 mbfmcnvima ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {{G}}^{-1}\left[{b}\right]\in {R}$
39 inelsiga ${⊢}\left({R}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {{F}}^{-1}\left[{a}\right]\in {R}\wedge {{G}}^{-1}\left[{b}\right]\in {R}\right)\to {{F}}^{-1}\left[{a}\right]\cap {{G}}^{-1}\left[{b}\right]\in {R}$
40 30 34 38 39 syl3anc ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {{F}}^{-1}\left[{a}\right]\cap {{G}}^{-1}\left[{b}\right]\in {R}$
41 29 40 eqeltrd ${⊢}\left({\phi }\wedge {a}\in {S}\wedge {b}\in {T}\right)\to {{H}}^{-1}\left[{a}×{b}\right]\in {R}$
42 25 26 27 41 syl3anc ${⊢}\left({\phi }\wedge \left({a}\in {S}\wedge {b}\in {T}\right)\wedge {c}={a}×{b}\right)\to {{H}}^{-1}\left[{a}×{b}\right]\in {R}$
43 24 42 eqeltrd ${⊢}\left({\phi }\wedge \left({a}\in {S}\wedge {b}\in {T}\right)\wedge {c}={a}×{b}\right)\to {{H}}^{-1}\left[{c}\right]\in {R}$
44 43 3expia ${⊢}\left({\phi }\wedge \left({a}\in {S}\wedge {b}\in {T}\right)\right)\to \left({c}={a}×{b}\to {{H}}^{-1}\left[{c}\right]\in {R}\right)$
45 44 rexlimdvva ${⊢}{\phi }\to \left(\exists {a}\in {S}\phantom{\rule{.4em}{0ex}}\exists {b}\in {T}\phantom{\rule{.4em}{0ex}}{c}={a}×{b}\to {{H}}^{-1}\left[{c}\right]\in {R}\right)$
46 45 imp ${⊢}\left({\phi }\wedge \exists {a}\in {S}\phantom{\rule{.4em}{0ex}}\exists {b}\in {T}\phantom{\rule{.4em}{0ex}}{c}={a}×{b}\right)\to {{H}}^{-1}\left[{c}\right]\in {R}$
47 22 46 sylan2b ${⊢}\left({\phi }\wedge {c}\in \mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)\right)\to {{H}}^{-1}\left[{c}\right]\in {R}$
48 47 ralrimiva ${⊢}{\phi }\to \forall {c}\in \mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)\phantom{\rule{.4em}{0ex}}{{H}}^{-1}\left[{c}\right]\in {R}$
49 eqid ${⊢}\mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)=\mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)$
50 49 txbasex ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to \mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)\in \mathrm{V}$
51 2 3 50 syl2anc ${⊢}{\phi }\to \mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)\in \mathrm{V}$
52 49 sxval ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {S}{×}_{s}{T}=𝛔\left(\mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)\right)$
53 2 3 52 syl2anc ${⊢}{\phi }\to {S}{×}_{s}{T}=𝛔\left(\mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)\right)$
54 51 1 53 imambfm ${⊢}{\phi }\to \left({H}\in \left({R}{\mathrm{MblFn}}_{\mu }\left({S}{×}_{s}{T}\right)\right)↔\left({H}:\bigcup {R}⟶\bigcup \left({S}{×}_{s}{T}\right)\wedge \forall {c}\in \mathrm{ran}\left({a}\in {S},{b}\in {T}⟼{a}×{b}\right)\phantom{\rule{.4em}{0ex}}{{H}}^{-1}\left[{c}\right]\in {R}\right)\right)$
55 17 48 54 mpbir2and ${⊢}{\phi }\to {H}\in \left({R}{\mathrm{MblFn}}_{\mu }\left({S}{×}_{s}{T}\right)\right)$