Theorem fndmfifsupp

Description: A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019)

	Ref	Expression
Hypotheses	fndmfisuppfi.f	⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
	fndmfisuppfi.d	⊢ ( 𝜑 → 𝐷 ∈ Fin )
	fndmfisuppfi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion	fndmfifsupp	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fndmfisuppfi.f	⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
2		fndmfisuppfi.d	⊢ ( 𝜑 → 𝐷 ∈ Fin )
3		fndmfisuppfi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4		dffn3	⊢ ( 𝐹 Fn 𝐷 ↔ 𝐹 : 𝐷 ⟶ ran 𝐹 )
5	1 4	sylib	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ran 𝐹 )
6	5 2 3	fdmfifsupp	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )