Theorem mbfmfun

Description: A measurable function is a function. (Contributed by Thierry Arnoux, 24-Jan-2017)

	Ref	Expression
Hypothesis	mbfmfun.1	$$⊢\phi \to F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$
Assertion	mbfmfun	$$⊢\phi \to \mathrm{Fun}F$$

Proof

Step	Hyp	Ref	Expression
1		mbfmfun.1	$$⊢\phi \to F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$
2		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)$$
3	2	biimpi	$$⊢F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }\to \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)$$
4		elmapfun	$$⊢F\in \left({\bigcup t}^{\bigcup s}\right)\to \mathrm{Fun}F$$
5	4	adantr	$$⊢\left(F\in \left({\bigcup t}^{\bigcup s}\right)\wedge \forall x\in t{F}^{-1}\left[x\right]\in s\right)\to \mathrm{Fun}F$$
6	5	rexlimivw	$$⊢\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)\to \mathrm{Fun}F$$
7	6	rexlimivw	$$⊢\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)\to \mathrm{Fun}F$$
8	1 3 7	3syl	$$⊢\phi \to \mathrm{Fun}F$$