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

Proof

Step	Hyp	Ref	Expression
1		smffmptf.x	⊢ Ⅎ 𝑥 𝜑
2		smffmptf.a	⊢ Ⅎ 𝑥 𝐴
3		smffmptf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smffmptf.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
5		smffmptf.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
6		eqid	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	3 5 6	smff	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℝ )
8	1 2 4	dmmpt1	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
9	8	eqcomd	⊢ ( 𝜑 → 𝐴 = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
10	9	feq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℝ ) )
11	7 10	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )