Theorem fdmfisuppfi

Description: The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019)

	Ref	Expression
Hypotheses	fdmfisuppfi.f	|- ( ph -> F : D --> R )
	fdmfisuppfi.d	|- ( ph -> D e. Fin )
	fdmfisuppfi.z	|- ( ph -> Z e. V )
Assertion	fdmfisuppfi	|- ( ph -> ( F supp Z ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		fdmfisuppfi.f	|- ( ph -> F : D --> R )
2		fdmfisuppfi.d	|- ( ph -> D e. Fin )
3		fdmfisuppfi.z	|- ( 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 )