Theorem smffmpt

Description: A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smffmpt.x	|- F/ x ph
	smffmpt.s	|- ( ph -> S e. SAlg )
	smffmpt.b	|- ( ( ph /\ x e. A ) -> B e. V )
	smffmpt.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
Assertion	smffmpt	|- ( ph -> ( x e. A |-> B ) : A --> RR )

Proof

Step	Hyp	Ref	Expression
1		smffmpt.x	|- F/ x ph
2		smffmpt.s	|- ( ph -> S e. SAlg )
3		smffmpt.b	|- ( ( ph /\ x e. A ) -> B e. V )
4		smffmpt.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
5		nfcv	|- F/_ x A
6	1 5 2 3 4	smffmptf	|- ( ph -> ( x e. A |-> B ) : A --> RR )