Theorem fidmfisupp

Description: A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	fidmfisupp.1	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
	fidmfisupp.2	⊢ ( 𝜑 → 𝐷 ∈ Fin )
	fidmfisupp.3	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion	fidmfisupp	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fidmfisupp.1	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
2		fidmfisupp.2	⊢ ( 𝜑 → 𝐷 ∈ Fin )
3		fidmfisupp.3	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
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 )
9	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
10		funisfsupp	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
11	9 4 3 10	syl3anc	⊢ ( 𝜑 → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
12	8 11	mpbird	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )