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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ) → ( 𝐹 ↾ 𝐵 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		resindm	⊢ ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐵 )
2		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
3	2	funfnd	⊢ ( 𝐹 Fn 𝐴 → 𝐹 Fn dom 𝐹 )
4		fnresin2	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) Fn ( 𝐵 ∩ dom 𝐹 ) )
5		infi	⊢ ( 𝐵 ∈ Fin → ( 𝐵 ∩ dom 𝐹 ) ∈ Fin )
6		fnfi	⊢ ( ( ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) Fn ( 𝐵 ∩ dom 𝐹 ) ∧ ( 𝐵 ∩ dom 𝐹 ) ∈ Fin ) → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin )
7	5 6	sylan2	⊢ ( ( ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) Fn ( 𝐵 ∩ dom 𝐹 ) ∧ 𝐵 ∈ Fin ) → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin )
8	7	ex	⊢ ( ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) Fn ( 𝐵 ∩ dom 𝐹 ) → ( 𝐵 ∈ Fin → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin ) )
9	3 4 8	3syl	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ Fin → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin ) )
10	9	imp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ) → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin )
11	1 10	eqeltrrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ) → ( 𝐹 ↾ 𝐵 ) ∈ Fin )