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		fex	⊢ ( ( 𝐹 : 𝐷 ⟶ 𝑅 ∧ 𝐷 ∈ Fin ) → 𝐹 ∈ V )
5	1 2 4	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
6		suppimacnv	⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
7	5 3 6	syl2anc	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
8	2 1	fisuppfi	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
9	7 8	eqeltrd	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )