Theorem fsuppmptdm

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

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

Proof

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