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

Proof

Step	Hyp	Ref	Expression
1		smffmptf.x	$$⊢Ⅎx\phi$$
2		smffmptf.a	$$⊢\underset{\_}{Ⅎ}xA$$
3		smffmptf.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		smffmptf.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
5		smffmptf.m	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
6		eqid	$$⊢\mathrm{dom}\left(x\in A⟼B\right)=\mathrm{dom}\left(x\in A⟼B\right)$$
7	3 5 6	smff	$$⊢\phi \to \left(x\in A⟼B\right):\mathrm{dom}\left(x\in A⟼B\right)⟶ℝ$$
8	1 2 4	dmmpt1	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼B\right)=A$$
9	8	eqcomd	$$⊢\phi \to A=\mathrm{dom}\left(x\in A⟼B\right)$$
10	9	feq2d	$$⊢\phi \to \left(\left(x\in A⟼B\right):A⟶ℝ\leftrightarrow \left(x\in A⟼B\right):\mathrm{dom}\left(x\in A⟼B\right)⟶ℝ\right)$$
11	7 10	mpbird	$$⊢\phi \to \left(x\in A⟼B\right):A⟶ℝ$$