Theorem mbfmf

Description: A measurable function as a function with domain and codomain. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypotheses	mbfmf.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	mbfmf.2	$$⊢\phi \to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	mbfmf.3	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
Assertion	mbfmf	$$⊢\phi \to F:\bigcup S⟶\bigcup T$$

Proof

Step	Hyp	Ref	Expression
1		mbfmf.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
2		mbfmf.2	$$⊢\phi \to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
3		mbfmf.3	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
4	1 2	ismbfm	$$⊢\phi \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)$$
5	3 4	mpbid	$$⊢\phi \to \left(F\in \left({\bigcup T}^{\bigcup S}\right)\wedge \forall x\in T{F}^{-1}\left[x\right]\in S\right)$$
6	5	simpld	$$⊢\phi \to F\in \left({\bigcup T}^{\bigcup S}\right)$$
7		elmapi	$$⊢F\in \left({\bigcup T}^{\bigcup S}\right)\to F:\bigcup S⟶\bigcup T$$
8	6 7	syl	$$⊢\phi \to F:\bigcup S⟶\bigcup T$$