Theorem resfsupp

Description: If the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finitely supported, the function itself is finitely supported. (Contributed by AV, 27-May-2019)

	Ref	Expression
Hypotheses	resfsupp.b	$$⊢\phi \to \mathrm{dom}F\setminus B\in \mathrm{Fin}$$
	resfsupp.e	$$⊢\phi \to F\in W$$
	resfsupp.f	$$⊢\phi \to \mathrm{Fun}F$$
	resfsupp.g	$$⊢\phi \to G={F\upharpoonright }_B$$
	resfsupp.s	$$⊢\phi \to {finSupp}_Z\left(G\right)$$
	resfsupp.z	$$⊢\phi \to Z\in V$$
Assertion	resfsupp	$$⊢\phi \to {finSupp}_Z\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		resfsupp.b	$$⊢\phi \to \mathrm{dom}F\setminus B\in \mathrm{Fin}$$
2		resfsupp.e	$$⊢\phi \to F\in W$$
3		resfsupp.f	$$⊢\phi \to \mathrm{Fun}F$$
4		resfsupp.g	$$⊢\phi \to G={F\upharpoonright }_B$$
5		resfsupp.s	$$⊢\phi \to {finSupp}_Z\left(G\right)$$
6		resfsupp.z	$$⊢\phi \to Z\in V$$
7	5	fsuppimpd	$$⊢\phi \to G\mathrm{supp}Z\in \mathrm{Fin}$$
8	1 2 4 7 6	ressuppfi	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$
9		funisfsupp	$$⊢\left(\mathrm{Fun}F\wedge F\in W\wedge Z\in V\right)\to \left({finSupp}_Z\left(F\right)\leftrightarrow F\mathrm{supp}Z\in \mathrm{Fin}\right)$$
10	3 2 6 9	syl3anc	$$⊢\phi \to \left({finSupp}_Z\left(F\right)\leftrightarrow F\mathrm{supp}Z\in \mathrm{Fin}\right)$$
11	8 10	mpbird	$$⊢\phi \to {finSupp}_Z\left(F\right)$$