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 }\leftrightarrow \exists s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\exists t\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\left(F\in \left({\bigcup t}^{\bigcup s}\right)\wedge \forall x\in t{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{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 }\leftrightarrow \exists a\in \mathrm{dom}{\mathrm{MblFn}}_{\mu }F\in {\mathrm{MblFn}}_{\mu }\left(a\right)\right)$$
4	2 3	ax-mp	$$⊢F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }\leftrightarrow \exists a\in \mathrm{dom}{\mathrm{MblFn}}_{\mu }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{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}\times \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
8	7	rexeqi	$$⊢\exists a\in \mathrm{dom}{\mathrm{MblFn}}_{\mu }F\in {\mathrm{MblFn}}_{\mu }\left(a\right)\leftrightarrow \exists a\in \left(\bigcup \mathrm{ran}\mathrm{sigAlgebra}\times \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)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	eqtr4di	$$⊢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)\leftrightarrow F\in \left(s{\mathrm{MblFn}}_{\mu }t\right)\right)$$
13	12	rexxp	$$⊢\exists a\in \left(\bigcup \mathrm{ran}\mathrm{sigAlgebra}\times \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)F\in {\mathrm{MblFn}}_{\mu }\left(a\right)\leftrightarrow \exists s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\exists t\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}F\in \left(s{\mathrm{MblFn}}_{\mu }t\right)$$
14	4 8 13	3bitri	$$⊢F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }\leftrightarrow \exists s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\exists t\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}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)\leftrightarrow \left(F\in \left({\bigcup t}^{\bigcup s}\right)\wedge \forall x\in t{F}^{-1}\left[x\right]\in s\right)\right)$$
18	17	2rexbiia	$$⊢\exists s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\exists t\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}F\in \left(s{\mathrm{MblFn}}_{\mu }t\right)\leftrightarrow \exists s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\exists t\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\left(F\in \left({\bigcup t}^{\bigcup s}\right)\wedge \forall x\in t{F}^{-1}\left[x\right]\in s\right)$$
19	14 18	bitri	$$⊢F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }\leftrightarrow \exists s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\exists t\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\left(F\in \left({\bigcup t}^{\bigcup s}\right)\wedge \forall x\in t{F}^{-1}\left[x\right]\in s\right)$$