Theorem smffmptf

Description: A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 5-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		smffmptf.x	|- F/ x ph
2		smffmptf.a	|- F/_ x A
3		smffmptf.s	|- ( ph -> S e. SAlg )
4		smffmptf.b	|- ( ( ph /\ x e. A ) -> B e. V )
5		smffmptf.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
6		eqid	|- dom ( x e. A |-> B ) = dom ( x e. A |-> B )
7	3 5 6	smff	|- ( ph -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> RR )
8	1 2 4	dmmpt1	|- ( ph -> dom ( x e. A |-> B ) = A )
9	8	eqcomd	|- ( ph -> A = dom ( x e. A |-> B ) )
10	9	feq2d	|- ( ph -> ( ( x e. A |-> B ) : A --> RR <-> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> RR ) )
11	7 10	mpbird	|- ( ph -> ( x e. A |-> B ) : A --> RR )