Metamath Proof Explorer

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 ∈ Fin → F ↾ B ∈ Fin

Proof

Step Hyp Ref Expression
1 fnrel ⊢ F Fn A → Rel ⁡ F
2 1 adantr ⊢ F Fn A ∧ B ∈ Fin → Rel ⁡ F
3 resindm ⊢ Rel ⁡ F → F ↾ B ∩ dom ⁡ F = F ↾ B
4 3 eqcomd ⊢ Rel ⁡ F → F ↾ B = F ↾ B ∩ dom ⁡ F
5 2 4 syl ⊢ F Fn A ∧ B ∈ Fin → F ↾ B = F ↾ B ∩ dom ⁡ F
6 fnfun ⊢ F Fn A → Fun ⁡ F
7 6 funfnd ⊢ F Fn A → F Fn dom ⁡ F
8 fnresin2 ⊢ F Fn dom ⁡ F → F ↾ B ∩ dom ⁡ F Fn B ∩ dom ⁡ F
9 infi ⊢ B ∈ Fin → B ∩ dom ⁡ F ∈ Fin
10 fnfi ⊢ F ↾ B ∩ dom ⁡ F Fn B ∩ dom ⁡ F ∧ B ∩ dom ⁡ F ∈ Fin → F ↾ B ∩ dom ⁡ F ∈ Fin
11 9 10 sylan2 ⊢ F ↾ B ∩ dom ⁡ F Fn B ∩ dom ⁡ F ∧ B ∈ Fin → F ↾ B ∩ dom ⁡ F ∈ Fin
12 11 ex ⊢ F ↾ B ∩ dom ⁡ F Fn B ∩ dom ⁡ F → B ∈ Fin → F ↾ B ∩ dom ⁡ F ∈ Fin
13 7 8 12 3syl ⊢ F Fn A → B ∈ Fin → F ↾ B ∩ dom ⁡ F ∈ Fin
14 13 imp ⊢ F Fn A ∧ B ∈ Fin → F ↾ B ∩ dom ⁡ F ∈ Fin
15 5 14 eqeltrd ⊢ F Fn A ∧ B ∈ Fin → F ↾ B ∈ Fin