Theorem fndmfisuppfi

Description: The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019)

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

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	fdmfisuppfi	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )