Theorem fsuppimpd

Description: A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019)

	Ref	Expression
Hypothesis	fsuppimpd.f	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
Assertion	fsuppimpd	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		fsuppimpd.f	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
2		fsuppimp	$$⊢{finSupp}_Z\left(F\right)\to \left(\mathrm{Fun}F\wedge F\mathrm{supp}Z\in \mathrm{Fin}\right)$$
3	2	simprd	$$⊢{finSupp}_Z\left(F\right)\to F\mathrm{supp}Z\in \mathrm{Fin}$$
4	1 3	syl	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$