resfifsupp

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

Step	Hyp	Ref	Expression
1		resfifsupp.f	$⊢ φ \to Fun F$
2		resfifsupp.x	$⊢ φ \to X \in Fin$
3		resfifsupp.z	$⊢ φ \to Z \in V$
4		funrel	$⊢ Fun F \to Rel F$
5	1 4	syl	$⊢ φ \to Rel F$
6		resindm	$⊢ Rel F \to {F ↾}_{(X \cap dom F)} = {F ↾}_{X}$
7	5 6	syl	$⊢ φ \to {F ↾}_{(X \cap dom F)} = {F ↾}_{X}$
8	1	funfnd	$⊢ φ \to F Fn dom F$
9		fnresin2	$⊢ F Fn dom F \to ({F ↾}_{(X \cap dom F)}) Fn (X \cap dom F)$
10	8 9	syl	$⊢ φ \to ({F ↾}_{(X \cap dom F)}) Fn (X \cap dom F)$
11		infi	$⊢ X \in Fin \to X \cap dom F \in Fin$
12	2 11	syl	$⊢ φ \to X \cap dom F \in Fin$
13	10 12 3	fndmfifsupp	$⊢ φ \to {finSupp}_{Z} (({F ↾}_{(X \cap dom F)}))$
14	7 13	eqbrtrrd	$⊢ φ \to {finSupp}_{Z} (({F ↾}_{X}))$

Metamath Proof Explorer