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	$$⊢Ⅎx\phi$$
	smffmpt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	smffmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	smffmpt.m	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
Assertion	smffmpt	$$⊢\phi \to \left(x\in A⟼B\right):A⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		smffmpt.x	$$⊢Ⅎx\phi$$
2		smffmpt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
3		smffmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
4		smffmpt.m	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
6	1 5 2 3 4	smffmptf	$$⊢\phi \to \left(x\in A⟼B\right):A⟶ℝ$$