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	|- ( ph -> S e. U. ran sigAlgebra )
	mbfmf.2	|- ( ph -> T e. U. ran sigAlgebra )
	mbfmf.3	|- ( ph -> F e. ( S MblFnM T ) )
Assertion	mbfmf	|- ( ph -> F : U. S --> U. T )

Proof

Step	Hyp	Ref	Expression
1		mbfmf.1	|- ( ph -> S e. U. ran sigAlgebra )
2		mbfmf.2	|- ( ph -> T e. U. ran sigAlgebra )
3		mbfmf.3	|- ( ph -> F e. ( S MblFnM T ) )
4	1 2	ismbfm	|- ( ph -> ( F e. ( S MblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) ) )
5	3 4	mpbid	|- ( ph -> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) )
6	5	simpld	|- ( ph -> F e. ( U. T ^m U. S ) )
7		elmapi	|- ( F e. ( U. T ^m U. S ) -> F : U. S --> U. T )
8	6 7	syl	|- ( ph -> F : U. S --> U. T )