Theorem fndmfifsupp

Description: A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019)

	Ref	Expression
Hypotheses	fndmfisuppfi.f	$$⊢\phi \to FFnD$$
	fndmfisuppfi.d	$$⊢\phi \to D\in \mathrm{Fin}$$
	fndmfisuppfi.z	$$⊢\phi \to Z\in V$$
Assertion	fndmfifsupp	$$⊢\phi \to {finSupp}_Z\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fndmfisuppfi.f	$$⊢\phi \to FFnD$$
2		fndmfisuppfi.d	$$⊢\phi \to D\in \mathrm{Fin}$$
3		fndmfisuppfi.z	$$⊢\phi \to Z\in V$$
4		dffn3	$$⊢FFnD\leftrightarrow F:D⟶\mathrm{ran}F$$
5	1 4	sylib	$$⊢\phi \to F:D⟶\mathrm{ran}F$$
6	5 2 3	fdmfifsupp	$$⊢\phi \to {finSupp}_Z\left(F\right)$$