Theorem fidmfisupp

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

	Ref	Expression
Hypotheses	fidmfisupp.1	|- ( ph -> F : D --> R )
	fidmfisupp.2	|- ( ph -> D e. Fin )
	fidmfisupp.3	|- ( ph -> Z e. V )
Assertion	fidmfisupp	|- ( ph -> F finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fidmfisupp.1	|- ( ph -> F : D --> R )
2		fidmfisupp.2	|- ( ph -> D e. Fin )
3		fidmfisupp.3	|- ( ph -> Z e. V )
4	1 2	fexd	|- ( ph -> F e. _V )
5		suppimacnv	|- ( ( F e. _V /\ Z e. V ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
6	4 3 5	syl2anc	|- ( ph -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
7	2 1	fisuppfi	|- ( ph -> ( `' F " ( _V \ { Z } ) ) e. Fin )
8	6 7	eqeltrd	|- ( ph -> ( F supp Z ) e. Fin )
9	1	ffund	|- ( ph -> Fun F )
10		funisfsupp	|- ( ( Fun F /\ F e. _V /\ Z e. V ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
11	9 4 3 10	syl3anc	|- ( ph -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
12	8 11	mpbird	|- ( ph -> F finSupp Z )