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	$$⊢\phi \to S\in \mathrm{SAlg}$$
	sssmfmpt.f	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
	sssmfmpt.c	$$⊢\phi \to C\subseteq A$$
Assertion	sssmfmpt	$$⊢\phi \to \left(x\in C⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		sssmfmpt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		sssmfmpt.f	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
3		sssmfmpt.c	$$⊢\phi \to C\subseteq A$$
4	3	resmptd	$$⊢\phi \to {\left(x\in A⟼B\right)\upharpoonright }_C=\left(x\in C⟼B\right)$$
5	4	eqcomd	$$⊢\phi \to \left(x\in C⟼B\right)={\left(x\in A⟼B\right)\upharpoonright }_C$$
6	1 2	sssmf	$$⊢\phi \to {\left(x\in A⟼B\right)\upharpoonright }_C\in \mathrm{SMblFn}\left(S\right)$$
7	5 6	eqeltrd	$$⊢\phi \to \left(x\in C⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$