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		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2	1	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ) → Rel 𝐹 )
3		resindm	⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐵 ) )
4	3	eqcomd	⊢ ( Rel 𝐹 → ( 𝐹 ↾ 𝐵 ) = ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) )
5	2 4	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ) → ( 𝐹 ↾ 𝐵 ) = ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) )
6		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
7	6	funfnd	⊢ ( 𝐹 Fn 𝐴 → 𝐹 Fn dom 𝐹 )
8		fnresin2	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) Fn ( 𝐵 ∩ dom 𝐹 ) )
9		infi	⊢ ( 𝐵 ∈ Fin → ( 𝐵 ∩ dom 𝐹 ) ∈ Fin )
10		fnfi	⊢ ( ( ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) Fn ( 𝐵 ∩ dom 𝐹 ) ∧ ( 𝐵 ∩ dom 𝐹 ) ∈ Fin ) → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin )
11	9 10	sylan2	⊢ ( ( ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) Fn ( 𝐵 ∩ dom 𝐹 ) ∧ 𝐵 ∈ Fin ) → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin )
12	11	ex	⊢ ( ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) Fn ( 𝐵 ∩ dom 𝐹 ) → ( 𝐵 ∈ Fin → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin ) )
13	7 8 12	3syl	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ Fin → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin ) )
14	13	imp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ) → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) ∈ Fin )
15	5 14	eqeltrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ) → ( 𝐹 ↾ 𝐵 ) ∈ Fin )