Theorem fndmfifsupp

Description: A function with a finite domain is always finitely supported. (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	fndmfifsupp	|- ( ph -> F finSupp Z )

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	fdmfifsupp	|- ( ph -> F finSupp Z )