Theorem resfifsupp

Description: The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019)

	Ref	Expression
Hypotheses	resfifsupp.f	$$⊢\phi \to \mathrm{Fun}F$$
	resfifsupp.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	resfifsupp.z	$$⊢\phi \to Z\in V$$
Assertion	resfifsupp	$$⊢\phi \to {finSupp}_Z\left(\left({F\upharpoonright }_X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		resfifsupp.f	$$⊢\phi \to \mathrm{Fun}F$$
2		resfifsupp.x	$$⊢\phi \to X\in \mathrm{Fin}$$
3		resfifsupp.z	$$⊢\phi \to Z\in V$$
4		resindm	$$⊢{F\upharpoonright }_{\left(X\cap \mathrm{dom}F\right)}={F\upharpoonright }_X$$
5	1	funfnd	$$⊢\phi \to FFn\mathrm{dom}F$$
6		fnresin2	$$⊢FFn\mathrm{dom}F\to \left({F\upharpoonright }_{\left(X\cap \mathrm{dom}F\right)}\right)Fn\left(X\cap \mathrm{dom}F\right)$$
7	5 6	syl	$$⊢\phi \to \left({F\upharpoonright }_{\left(X\cap \mathrm{dom}F\right)}\right)Fn\left(X\cap \mathrm{dom}F\right)$$
8		infi	$$⊢X\in \mathrm{Fin}\to X\cap \mathrm{dom}F\in \mathrm{Fin}$$
9	2 8	syl	$$⊢\phi \to X\cap \mathrm{dom}F\in \mathrm{Fin}$$
10	7 9 3	fndmfifsupp	$$⊢\phi \to {finSupp}_Z\left(\left({F\upharpoonright }_{\left(X\cap \mathrm{dom}F\right)}\right)\right)$$
11	4 10	eqbrtrrid	$$⊢\phi \to {finSupp}_Z\left(\left({F\upharpoonright }_X\right)\right)$$