Theorem resfifsupp

Description: The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019)

	Ref	Expression
Hypotheses	resfifsupp.f	|- ( ph -> Fun F )
	resfifsupp.x	|- ( ph -> X e. Fin )
	resfifsupp.z	|- ( ph -> Z e. V )
Assertion	resfifsupp	|- ( ph -> ( F |` X ) finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		resfifsupp.f	|- ( ph -> Fun F )
2		resfifsupp.x	|- ( ph -> X e. Fin )
3		resfifsupp.z	|- ( ph -> Z e. V )
4		resindm	|- ( F |` ( X i^i dom F ) ) = ( F |` X )
5	1	funfnd	|- ( ph -> F Fn dom F )
6		fnresin2	|- ( F Fn dom F -> ( F |` ( X i^i dom F ) ) Fn ( X i^i dom F ) )
7	5 6	syl	|- ( ph -> ( F |` ( X i^i dom F ) ) Fn ( X i^i dom F ) )
8		infi	|- ( X e. Fin -> ( X i^i dom F ) e. Fin )
9	2 8	syl	|- ( ph -> ( X i^i dom F ) e. Fin )
10	7 9 3	fndmfifsupp	|- ( ph -> ( F |` ( X i^i dom F ) ) finSupp Z )
11	4 10	eqbrtrrid	|- ( ph -> ( F |` X ) finSupp Z )