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		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 )
10	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
11		funisfsupp	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
12	10 5 3 11	syl3anc	⊢ ( 𝜑 → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
13	9 12	mpbird	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )