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	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 )