Theorem fdmfisuppfi

Description: The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019)

	Ref	Expression
Hypotheses	fdmfisuppfi.f	$$⊢\phi \to F:D⟶R$$
	fdmfisuppfi.d	$$⊢\phi \to D\in \mathrm{Fin}$$
	fdmfisuppfi.z	$$⊢\phi \to Z\in V$$
Assertion	fdmfisuppfi	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		fdmfisuppfi.f	$$⊢\phi \to F:D⟶R$$
2		fdmfisuppfi.d	$$⊢\phi \to D\in \mathrm{Fin}$$
3		fdmfisuppfi.z	$$⊢\phi \to Z\in V$$
4	1 2	fexd	$$⊢\phi \to F\in \mathrm{V}$$
5		suppimacnv	$$⊢\left(F\in \mathrm{V}\wedge Z\in V\right)\to F\mathrm{supp}Z=F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
6	4 3 5	syl2anc	$$⊢\phi \to F\mathrm{supp}Z=F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
7	2 1	fisuppfi	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$
8	6 7	eqeltrd	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$