Theorem fsuppfund

Description: A finitely supported function is a function. (Contributed by SN, 8-Mar-2025)

	Ref	Expression
Hypothesis	fsuppfund.1	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
Assertion	fsuppfund	$$⊢\phi \to \mathrm{Fun}F$$

Proof

Step	Hyp	Ref	Expression
1		fsuppfund.1	$$⊢\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	simpld	$$⊢{finSupp}_Z\left(F\right)\to \mathrm{Fun}F$$
4	1 3	syl	$$⊢\phi \to \mathrm{Fun}F$$