Theorem fdmfifsupp

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

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

Proof

Step	Hyp	Ref	Expression
1		fdmfisuppfi.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
2		fdmfisuppfi.d	⊢ ( 𝜑 → 𝐷 ∈ Fin )
3		fdmfisuppfi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
5	1 2 3	fdmfisuppfi	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
6	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
7		fnex	⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝐷 ∈ Fin ) → 𝐹 ∈ V )
8	6 2 7	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
9		isfsupp	⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 ↔ ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) ) )
10	8 3 9	syl2anc	⊢ ( 𝜑 → ( 𝐹 finSupp 𝑍 ↔ ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) ) )
11	4 5 10	mpbir2and	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )