Theorem fndmfisuppfi

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

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

Proof

Step	Hyp	Ref	Expression
1		fndmfisuppfi.f	|- ( ph -> F Fn D )
2		fndmfisuppfi.d	|- ( ph -> D e. Fin )
3		fndmfisuppfi.z	|- ( ph -> Z e. V )
4		dffn3	|- ( F Fn D <-> F : D --> ran F )
5	1 4	sylib	|- ( ph -> F : D --> ran F )
6	5 2 3	fdmfisuppfi	|- ( ph -> ( F supp Z ) e. Fin )