resfnfinfin

Description: The restriction of a function to a finite set is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018)

		Ref	Expression
	Assertion	resfnfinfin	$⊢ (F Fn A \land B \in Fin) \to {F ↾}_{B} \in Fin$

Step	Hyp	Ref	Expression
1		fnrel	$⊢ F Fn A \to Rel F$
2	1	adantr	$⊢ (F Fn A \land B \in Fin) \to Rel F$
3		resindm	$⊢ Rel F \to {F ↾}_{(B \cap dom F)} = {F ↾}_{B}$
4	3	eqcomd	$⊢ Rel F \to {F ↾}_{B} = {F ↾}_{(B \cap dom F)}$
5	2 4	syl	$⊢ (F Fn A \land B \in Fin) \to {F ↾}_{B} = {F ↾}_{(B \cap dom F)}$
6		fnfun	$⊢ F Fn A \to Fun F$
7	6	funfnd	$⊢ F Fn A \to F Fn dom F$
8		fnresin2	$⊢ F Fn dom F \to ({F ↾}_{(B \cap dom F)}) Fn (B \cap dom F)$
9		infi	$⊢ B \in Fin \to B \cap dom F \in Fin$
10		fnfi	$⊢ (({F ↾}_{(B \cap dom F)}) Fn (B \cap dom F) \land B \cap dom F \in Fin) \to {F ↾}_{(B \cap dom F)} \in Fin$
11	9 10	sylan2	$⊢ (({F ↾}_{(B \cap dom F)}) Fn (B \cap dom F) \land B \in Fin) \to {F ↾}_{(B \cap dom F)} \in Fin$
12	11	ex	$⊢ ({F ↾}_{(B \cap dom F)}) Fn (B \cap dom F) \to (B \in Fin \to {F ↾}_{(B \cap dom F)} \in Fin)$
13	7 8 12	3syl	$⊢ F Fn A \to (B \in Fin \to {F ↾}_{(B \cap dom F)} \in Fin)$
14	13	imp	$⊢ (F Fn A \land B \in Fin) \to {F ↾}_{(B \cap dom F)} \in Fin$
15	5 14	eqeltrd	$⊢ (F Fn A \land B \in Fin) \to {F ↾}_{B} \in Fin$

Metamath Proof Explorer