Theorem mbfmfun

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

	Ref	Expression
Hypothesis	mbfmfun.1	|- ( ph -> F e. U. ran MblFnM )
Assertion	mbfmfun	|- ( ph -> Fun F )

Proof

Step	Hyp	Ref	Expression
1		mbfmfun.1	|- ( ph -> F e. U. ran MblFnM )
2		elunirnmbfm	|- ( F e. U. ran MblFnM <-> E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) )
3	2	biimpi	|- ( F e. U. ran MblFnM -> E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) )
4		elmapfun	|- ( F e. ( U. t ^m U. s ) -> Fun F )
5	4	adantr	|- ( ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) -> Fun F )
6	5	rexlimivw	|- ( E. t e. U. ran sigAlgebra ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) -> Fun F )
7	6	rexlimivw	|- ( E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) -> Fun F )
8	1 3 7	3syl	|- ( ph -> Fun F )