Theorem fidmfisupp

Description: A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	fidmfisupp.1	$$⊢\phi \to F:D⟶R$$
	fidmfisupp.2	$$⊢\phi \to D\in \mathrm{Fin}$$
	fidmfisupp.3	$$⊢\phi \to Z\in V$$
Assertion	fidmfisupp	$$⊢\phi \to {finSupp}_Z\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fidmfisupp.1	$$⊢\phi \to F:D⟶R$$
2		fidmfisupp.2	$$⊢\phi \to D\in \mathrm{Fin}$$
3		fidmfisupp.3	$$⊢\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}$$
10	1	ffund	$$⊢\phi \to \mathrm{Fun}F$$
11		funisfsupp	$$⊢\left(\mathrm{Fun}F\wedge F\in \mathrm{V}\wedge Z\in V\right)\to \left({finSupp}_Z\left(F\right)\leftrightarrow F\mathrm{supp}Z\in \mathrm{Fin}\right)$$
12	10 5 3 11	syl3anc	$$⊢\phi \to \left({finSupp}_Z\left(F\right)\leftrightarrow F\mathrm{supp}Z\in \mathrm{Fin}\right)$$
13	9 12	mpbird	$$⊢\phi \to {finSupp}_Z\left(F\right)$$