This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 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 )