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	⊢ Ⅎ 𝑥 𝜑
	smffmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smffmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	smffmpt.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
Assertion	smffmpt	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		smffmpt.x	⊢ Ⅎ 𝑥 𝜑
2		smffmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smffmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4		smffmpt.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
5		nfcv	⊢ Ⅎ 𝑥 𝐴
6	1 5 2 3 4	smffmptf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )