Theorem sssmfmpt

Description: The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	sssmfmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	sssmfmpt.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
	sssmfmpt.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
Assertion	sssmfmpt	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		sssmfmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		sssmfmpt.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
3		sssmfmpt.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4	3	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
5	4	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) )
6	1 2	sssmf	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) ∈ ( SMblFn ‘ 𝑆 ) )
7	5 6	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )