# Metamath Proof Explorer

## Theorem ismbfm

Description: The predicate " F is a measurable function from the measurable space S to the measurable space T ". Cf. ismbf . (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Hypotheses ismbfm.1 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
ismbfm.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
Assertion ismbfm ${⊢}{\phi }\to \left({F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)↔\left({F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\wedge \forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ismbfm.1 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
2 ismbfm.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 unieq ${⊢}{s}={S}\to \bigcup {s}=\bigcup {S}$
4 3 oveq2d ${⊢}{s}={S}\to {\bigcup {t}}^{\bigcup {s}}={\bigcup {t}}^{\bigcup {S}}$
5 eleq2 ${⊢}{s}={S}\to \left({{f}}^{-1}\left[{x}\right]\in {s}↔{{f}}^{-1}\left[{x}\right]\in {S}\right)$
6 5 ralbidv ${⊢}{s}={S}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {s}↔\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right)$
7 4 6 rabeqbidv ${⊢}{s}={S}\to \left\{{f}\in \left({\bigcup {t}}^{\bigcup {s}}\right)|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {s}\right\}=\left\{{f}\in \left({\bigcup {t}}^{\bigcup {S}}\right)|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right\}$
8 unieq ${⊢}{t}={T}\to \bigcup {t}=\bigcup {T}$
9 8 oveq1d ${⊢}{t}={T}\to {\bigcup {t}}^{\bigcup {S}}={\bigcup {T}}^{\bigcup {S}}$
10 raleq ${⊢}{t}={T}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}↔\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right)$
11 9 10 rabeqbidv ${⊢}{t}={T}\to \left\{{f}\in \left({\bigcup {t}}^{\bigcup {S}}\right)|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right\}=\left\{{f}\in \left({\bigcup {T}}^{\bigcup {S}}\right)|\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right\}$
12 df-mbfm ${⊢}{\mathrm{MblFn}}_{\mu }=\left({s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra},{t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}⟼\left\{{f}\in \left({\bigcup {t}}^{\bigcup {s}}\right)|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {s}\right\}\right)$
13 ovex ${⊢}{\bigcup {T}}^{\bigcup {S}}\in \mathrm{V}$
14 13 rabex ${⊢}\left\{{f}\in \left({\bigcup {T}}^{\bigcup {S}}\right)|\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right\}\in \mathrm{V}$
15 7 11 12 14 ovmpo ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {S}{\mathrm{MblFn}}_{\mu }{T}=\left\{{f}\in \left({\bigcup {T}}^{\bigcup {S}}\right)|\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right\}$
16 1 2 15 syl2anc ${⊢}{\phi }\to {S}{\mathrm{MblFn}}_{\mu }{T}=\left\{{f}\in \left({\bigcup {T}}^{\bigcup {S}}\right)|\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right\}$
17 16 eleq2d ${⊢}{\phi }\to \left({F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)↔{F}\in \left\{{f}\in \left({\bigcup {T}}^{\bigcup {S}}\right)|\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right\}\right)$
18 cnveq ${⊢}{f}={F}\to {{f}}^{-1}={{F}}^{-1}$
19 18 imaeq1d ${⊢}{f}={F}\to {{f}}^{-1}\left[{x}\right]={{F}}^{-1}\left[{x}\right]$
20 19 eleq1d ${⊢}{f}={F}\to \left({{f}}^{-1}\left[{x}\right]\in {S}↔{{F}}^{-1}\left[{x}\right]\in {S}\right)$
21 20 ralbidv ${⊢}{f}={F}\to \left(\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}↔\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}\right)$
22 21 elrab ${⊢}{F}\in \left\{{f}\in \left({\bigcup {T}}^{\bigcup {S}}\right)|\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in {S}\right\}↔\left({F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\wedge \forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}\right)$
23 17 22 syl6bb ${⊢}{\phi }\to \left({F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)↔\left({F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\wedge \forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}\right)\right)$