Theorem fdmfifsupp

Description: A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-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	fdmfifsupp	$$⊢\phi \to {finSupp}_Z\left(F\right)$$

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	ffund	$$⊢\phi \to \mathrm{Fun}F$$
5	1 2 3	fdmfisuppfi	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$
6	1	ffnd	$$⊢\phi \to FFnD$$
7		fnex	$$⊢\left(FFnD\wedge D\in \mathrm{Fin}\right)\to F\in \mathrm{V}$$
8	6 2 7	syl2anc	$$⊢\phi \to F\in \mathrm{V}$$
9		isfsupp	$$⊢\left(F\in \mathrm{V}\wedge Z\in V\right)\to \left({finSupp}_Z\left(F\right)\leftrightarrow \left(\mathrm{Fun}F\wedge F\mathrm{supp}Z\in \mathrm{Fin}\right)\right)$$
10	8 3 9	syl2anc	$$⊢\phi \to \left({finSupp}_Z\left(F\right)\leftrightarrow \left(\mathrm{Fun}F\wedge F\mathrm{supp}Z\in \mathrm{Fin}\right)\right)$$
11	4 5 10	mpbir2and	$$⊢\phi \to {finSupp}_Z\left(F\right)$$