Theorem fsuppmptdmf

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

	Ref	Expression
Hypotheses	fsuppmptdmf.n	⊢ Ⅎ 𝑥 𝜑
	fsuppmptdmf.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑌 )
	fsuppmptdmf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsuppmptdmf.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝑉 )
	fsuppmptdmf.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
Assertion	fsuppmptdmf	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fsuppmptdmf.n	⊢ Ⅎ 𝑥 𝜑
2		fsuppmptdmf.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑌 )
3		fsuppmptdmf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		fsuppmptdmf.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝑉 )
5		fsuppmptdmf.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
6	1 4 2	fmptdf	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑉 )
7	6 3 5	fdmfifsupp	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )