Theorem fdmfisuppfi

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

	Ref	Expression
Hypotheses	fdmfisuppfi.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
	fdmfisuppfi.d	⊢ ( 𝜑 → 𝐷 ∈ Fin )
	fdmfisuppfi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion	fdmfisuppfi	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fdmfisuppfi.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
2		fdmfisuppfi.d	⊢ ( 𝜑 → 𝐷 ∈ Fin )
3		fdmfisuppfi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4	1 2	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
5		suppimacnv	⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
6	4 3 5	syl2anc	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
7	2 1	fisuppfi	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
8	6 7	eqeltrd	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )