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		funrel	$$⊢\mathrm{Fun}F\to \mathrm{Rel}F$$
5	1 4	syl	$$⊢\phi \to \mathrm{Rel}F$$
6		resindm	$$⊢\mathrm{Rel}F\to {F\upharpoonright }_{\left(X\cap \mathrm{dom}F\right)}={F\upharpoonright }_X$$
7	5 6	syl	$$⊢\phi \to {F\upharpoonright }_{\left(X\cap \mathrm{dom}F\right)}={F\upharpoonright }_X$$
8	1	funfnd	$$⊢\phi \to FFn\mathrm{dom}F$$
9		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)$$
10	8 9	syl	$$⊢\phi \to \left({F\upharpoonright }_{\left(X\cap \mathrm{dom}F\right)}\right)Fn\left(X\cap \mathrm{dom}F\right)$$
11		infi	$$⊢X\in \mathrm{Fin}\to X\cap \mathrm{dom}F\in \mathrm{Fin}$$
12	2 11	syl	$$⊢\phi \to X\cap \mathrm{dom}F\in \mathrm{Fin}$$
13	10 12 3	fndmfifsupp	$$⊢\phi \to {finSupp}_Z\left(\left({F\upharpoonright }_{\left(X\cap \mathrm{dom}F\right)}\right)\right)$$
14	7 13	eqbrtrrd	$$⊢\phi \to {finSupp}_Z\left(\left({F\upharpoonright }_X\right)\right)$$