Theorem fssrescdmd

Description: Restriction of a function to a subclass of its domain as a function with domain and codomain. (Contributed by AV, 13-May-2025)

	Ref	Expression
Hypotheses	fssrescdmd.f	$$⊢\phi \to F:A⟶B$$
	fssrescdmd.c	$$⊢\phi \to C\subseteq A$$
	fssrescdmd.d	$$⊢\phi \to F\left[C\right]\subseteq D$$
Assertion	fssrescdmd	$$⊢\phi \to \left({F\upharpoonright }_C\right):C⟶D$$

Proof

Step	Hyp	Ref	Expression
1		fssrescdmd.f	$$⊢\phi \to F:A⟶B$$
2		fssrescdmd.c	$$⊢\phi \to C\subseteq A$$
3		fssrescdmd.d	$$⊢\phi \to F\left[C\right]\subseteq D$$
4	1	ffnd	$$⊢\phi \to FFnA$$
5	4 2	fnssresd	$$⊢\phi \to \left({F\upharpoonright }_C\right)FnC$$
6		resima	$$⊢\left({F\upharpoonright }_C\right)\left[C\right]=F\left[C\right]$$
7	6 3	eqsstrid	$$⊢\phi \to \left({F\upharpoonright }_C\right)\left[C\right]\subseteq D$$
8	1	ffund	$$⊢\phi \to \mathrm{Fun}F$$
9	8	funresd	$$⊢\phi \to \mathrm{Fun}\left({F\upharpoonright }_C\right)$$
10	1	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
11	2 10	sseqtrrd	$$⊢\phi \to C\subseteq \mathrm{dom}F$$
12		ssdmres	$$⊢C\subseteq \mathrm{dom}F\leftrightarrow \mathrm{dom}\left({F\upharpoonright }_C\right)=C$$
13	12	a1i	$$⊢\phi \to \left(C\subseteq \mathrm{dom}F\leftrightarrow \mathrm{dom}\left({F\upharpoonright }_C\right)=C\right)$$
14		eqcom	$$⊢\mathrm{dom}\left({F\upharpoonright }_C\right)=C\leftrightarrow C=\mathrm{dom}\left({F\upharpoonright }_C\right)$$
15	13 14	bitrdi	$$⊢\phi \to \left(C\subseteq \mathrm{dom}F\leftrightarrow C=\mathrm{dom}\left({F\upharpoonright }_C\right)\right)$$
16	11 15	mpbid	$$⊢\phi \to C=\mathrm{dom}\left({F\upharpoonright }_C\right)$$
17	16	eqimssd	$$⊢\phi \to C\subseteq \mathrm{dom}\left({F\upharpoonright }_C\right)$$
18		funimass4	$$⊢\left(\mathrm{Fun}\left({F\upharpoonright }_C\right)\wedge C\subseteq \mathrm{dom}\left({F\upharpoonright }_C\right)\right)\to \left(\left({F\upharpoonright }_C\right)\left[C\right]\subseteq D\leftrightarrow \forall x\in C\left({F\upharpoonright }_C\right)\left(x\right)\in D\right)$$
19	9 17 18	syl2anc	$$⊢\phi \to \left(\left({F\upharpoonright }_C\right)\left[C\right]\subseteq D\leftrightarrow \forall x\in C\left({F\upharpoonright }_C\right)\left(x\right)\in D\right)$$
20	7 19	mpbid	$$⊢\phi \to \forall x\in C\left({F\upharpoonright }_C\right)\left(x\right)\in D$$
21		ffnfv	$$⊢\left({F\upharpoonright }_C\right):C⟶D\leftrightarrow \left(\left({F\upharpoonright }_C\right)FnC\wedge \forall x\in C\left({F\upharpoonright }_C\right)\left(x\right)\in D\right)$$
22	5 20 21	sylanbrc	$$⊢\phi \to \left({F\upharpoonright }_C\right):C⟶D$$