Theorem fsuppimpd

Description: A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019)

	Ref	Expression
Hypothesis	fsuppimpd.f	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
Assertion	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fsuppimpd.f	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
2		fsuppimp	⊢ ( 𝐹 finSupp 𝑍 → ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
3	2	simprd	⊢ ( 𝐹 finSupp 𝑍 → ( 𝐹 supp 𝑍 ) ∈ Fin )
4	1 3	syl	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )