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		fex	$$⊢\left(F:D⟶R\wedge D\in \mathrm{Fin}\right)\to F\in \mathrm{V}$$
5	1 2 4	syl2anc	$$⊢\phi \to F\in \mathrm{V}$$
6		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]$$
7	5 3 6	syl2anc	$$⊢\phi \to F\mathrm{supp}Z=F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
8	2 1	fisuppfi	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$
9	7 8	eqeltrd	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$