Theorem fsuppmptdmf

Description: A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019)

	Ref	Expression
Hypotheses	fsuppmptdmf.n	$$⊢Ⅎx\phi$$
	fsuppmptdmf.f	$$⊢F=\left(x\in A⟼Y\right)$$
	fsuppmptdmf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsuppmptdmf.y	$$⊢\left(\phi \wedge x\in A\right)\to Y\in V$$
	fsuppmptdmf.z	$$⊢\phi \to Z\in W$$
Assertion	fsuppmptdmf	$$⊢\phi \to {finSupp}_Z\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsuppmptdmf.n	$$⊢Ⅎx\phi$$
2		fsuppmptdmf.f	$$⊢F=\left(x\in A⟼Y\right)$$
3		fsuppmptdmf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
4		fsuppmptdmf.y	$$⊢\left(\phi \wedge x\in A\right)\to Y\in V$$
5		fsuppmptdmf.z	$$⊢\phi \to Z\in W$$
6	1 4 2	fmptdf	$$⊢\phi \to F:A⟶V$$
7	6 3 5	fdmfifsupp	$$⊢\phi \to {finSupp}_Z\left(F\right)$$