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		funrel	|- ( Fun F -> Rel F )
5	1 4	syl	|- ( ph -> Rel F )
6		resindm	|- ( Rel F -> ( F |` ( X i^i dom F ) ) = ( F |` X ) )
7	5 6	syl	|- ( ph -> ( F |` ( X i^i dom F ) ) = ( F |` X ) )
8	1	funfnd	|- ( ph -> F Fn dom F )
9		fnresin2	|- ( F Fn dom F -> ( F |` ( X i^i dom F ) ) Fn ( X i^i dom F ) )
10	8 9	syl	|- ( ph -> ( F |` ( X i^i dom F ) ) Fn ( X i^i dom F ) )
11		infi	|- ( X e. Fin -> ( X i^i dom F ) e. Fin )
12	2 11	syl	|- ( ph -> ( X i^i dom F ) e. Fin )
13	10 12 3	fndmfifsupp	|- ( ph -> ( F |` ( X i^i dom F ) ) finSupp Z )
14	7 13	eqbrtrrd	|- ( ph -> ( F |` X ) finSupp Z )