Theorem 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 /\ B e. Fin ) -> ( F |` B ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		resindm	|- ( F |` ( B i^i dom F ) ) = ( F |` B )
2		fnfun	|- ( F Fn A -> Fun F )
3	2	funfnd	|- ( F Fn A -> F Fn dom F )
4		fnresin2	|- ( F Fn dom F -> ( F |` ( B i^i dom F ) ) Fn ( B i^i dom F ) )
5		infi	|- ( B e. Fin -> ( B i^i dom F ) e. Fin )
6		fnfi	|- ( ( ( F |` ( B i^i dom F ) ) Fn ( B i^i dom F ) /\ ( B i^i dom F ) e. Fin ) -> ( F |` ( B i^i dom F ) ) e. Fin )
7	5 6	sylan2	|- ( ( ( F |` ( B i^i dom F ) ) Fn ( B i^i dom F ) /\ B e. Fin ) -> ( F |` ( B i^i dom F ) ) e. Fin )
8	7	ex	|- ( ( F |` ( B i^i dom F ) ) Fn ( B i^i dom F ) -> ( B e. Fin -> ( F |` ( B i^i dom F ) ) e. Fin ) )
9	3 4 8	3syl	|- ( F Fn A -> ( B e. Fin -> ( F |` ( B i^i dom F ) ) e. Fin ) )
10	9	imp	|- ( ( F Fn A /\ B e. Fin ) -> ( F |` ( B i^i dom F ) ) e. Fin )
11	1 10	eqeltrrid	|- ( ( F Fn A /\ B e. Fin ) -> ( F |` B ) e. Fin )