Theorem fndmfisuppfi

Description: The support of a function with a finite domain is always finite. (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	fndmfisuppfi	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$

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	fdmfisuppfi	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$