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	|- ( ph -> S e. SAlg )
	sssmfmpt.f	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
	sssmfmpt.c	|- ( ph -> C C_ A )
Assertion	sssmfmpt	|- ( ph -> ( x e. C |-> B ) e. ( SMblFn ` S ) )

Proof

Step	Hyp	Ref	Expression
1		sssmfmpt.s	|- ( ph -> S e. SAlg )
2		sssmfmpt.f	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
3		sssmfmpt.c	|- ( ph -> C C_ A )
4	3	resmptd	|- ( ph -> ( ( x e. A |-> B ) |` C ) = ( x e. C |-> B ) )
5	4	eqcomd	|- ( ph -> ( x e. C |-> B ) = ( ( x e. A |-> B ) |` C ) )
6	1 2	sssmf	|- ( ph -> ( ( x e. A |-> B ) |` C ) e. ( SMblFn ` S ) )
7	5 6	eqeltrd	|- ( ph -> ( x e. C |-> B ) e. ( SMblFn ` S ) )