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		resindm	$⊢ {F ↾}_{(B \cap dom F)} = {F ↾}_{B}$
2		fnfun	$⊢ F Fn A \to Fun F$
3	2	funfnd	$⊢ F Fn A \to F Fn dom F$
4		fnresin2	$⊢ F Fn dom F \to ({F ↾}_{(B \cap dom F)}) Fn (B \cap dom F)$
5		infi	$⊢ B \in Fin \to B \cap dom F \in Fin$
6		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$
7	5 6	sylan2	$⊢ (({F ↾}_{(B \cap dom F)}) Fn (B \cap dom F) \land B \in Fin) \to {F ↾}_{(B \cap dom F)} \in Fin$
8	7	ex	$⊢ ({F ↾}_{(B \cap dom F)}) Fn (B \cap dom F) \to (B \in Fin \to {F ↾}_{(B \cap dom F)} \in Fin)$
9	3 4 8	3syl	$⊢ F Fn A \to (B \in Fin \to {F ↾}_{(B \cap dom F)} \in Fin)$
10	9	imp	$⊢ (F Fn A \land B \in Fin) \to {F ↾}_{(B \cap dom F)} \in Fin$
11	1 10	eqeltrrid	$⊢ (F Fn A \land B \in Fin) \to {F ↾}_{B} \in Fin$

Metamath Proof Explorer