# Metamath Proof Explorer

## Theorem elunirnmbfm

Description: The property of being a measurable function. (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Assertion elunirnmbfm ${⊢}{F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }↔\exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\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)$

### Proof

Step Hyp Ref Expression
1 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)$
2 1 mpofun ${⊢}\mathrm{Fun}{\mathrm{MblFn}}_{\mu }$
3 elunirn ${⊢}\mathrm{Fun}{\mathrm{MblFn}}_{\mu }\to \left({F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }↔\exists {a}\in \mathrm{dom}{\mathrm{MblFn}}_{\mu }\phantom{\rule{.4em}{0ex}}{F}\in {\mathrm{MblFn}}_{\mu }\left({a}\right)\right)$
4 2 3 ax-mp ${⊢}{F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }↔\exists {a}\in \mathrm{dom}{\mathrm{MblFn}}_{\mu }\phantom{\rule{.4em}{0ex}}{F}\in {\mathrm{MblFn}}_{\mu }\left({a}\right)$
5 ovex ${⊢}{\bigcup {t}}^{\bigcup {s}}\in \mathrm{V}$
6 5 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}$
7 1 6 dmmpo ${⊢}\mathrm{dom}{\mathrm{MblFn}}_{\mu }=\bigcup \mathrm{ran}\mathrm{sigAlgebra}×\bigcup \mathrm{ran}\mathrm{sigAlgebra}$
8 7 rexeqi ${⊢}\exists {a}\in \mathrm{dom}{\mathrm{MblFn}}_{\mu }\phantom{\rule{.4em}{0ex}}{F}\in {\mathrm{MblFn}}_{\mu }\left({a}\right)↔\exists {a}\in \left(\bigcup \mathrm{ran}\mathrm{sigAlgebra}×\bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\phantom{\rule{.4em}{0ex}}{F}\in {\mathrm{MblFn}}_{\mu }\left({a}\right)$
9 fveq2 ${⊢}{a}=⟨{s},{t}⟩\to {\mathrm{MblFn}}_{\mu }\left({a}\right)={\mathrm{MblFn}}_{\mu }\left(⟨{s},{t}⟩\right)$
10 df-ov ${⊢}{s}{\mathrm{MblFn}}_{\mu }{t}={\mathrm{MblFn}}_{\mu }\left(⟨{s},{t}⟩\right)$
11 9 10 syl6eqr ${⊢}{a}=⟨{s},{t}⟩\to {\mathrm{MblFn}}_{\mu }\left({a}\right)={s}{\mathrm{MblFn}}_{\mu }{t}$
12 11 eleq2d ${⊢}{a}=⟨{s},{t}⟩\to \left({F}\in {\mathrm{MblFn}}_{\mu }\left({a}\right)↔{F}\in \left({s}{\mathrm{MblFn}}_{\mu }{t}\right)\right)$
13 12 rexxp ${⊢}\exists {a}\in \left(\bigcup \mathrm{ran}\mathrm{sigAlgebra}×\bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\phantom{\rule{.4em}{0ex}}{F}\in {\mathrm{MblFn}}_{\mu }\left({a}\right)↔\exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}{F}\in \left({s}{\mathrm{MblFn}}_{\mu }{t}\right)$
14 4 8 13 3bitri ${⊢}{F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }↔\exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}{F}\in \left({s}{\mathrm{MblFn}}_{\mu }{t}\right)$
15 simpl ${⊢}\left({s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
16 simpr ${⊢}\left({s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
17 15 16 ismbfm ${⊢}\left({s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\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)$
18 17 2rexbiia ${⊢}\exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}{F}\in \left({s}{\mathrm{MblFn}}_{\mu }{t}\right)↔\exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\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)$
19 14 18 bitri ${⊢}{F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }↔\exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\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)$