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