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

Proof

Step Hyp Ref Expression
1 fnrel 
 |-  ( F Fn A -> Rel F )
2 1 adantr 
 |-  ( ( F Fn A /\ B e. Fin ) -> Rel F )
3 resindm 
 |-  ( Rel F -> ( F |` ( B i^i dom F ) ) = ( F |` B ) )
4 3 eqcomd 
 |-  ( Rel F -> ( F |` B ) = ( F |` ( B i^i dom F ) ) )
5 2 4 syl 
 |-  ( ( F Fn A /\ B e. Fin ) -> ( F |` B ) = ( F |` ( B i^i 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 i^i dom F ) ) Fn ( B i^i dom F ) )
9 infi 
 |-  ( B e. Fin -> ( B i^i dom F ) e. Fin )
10 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 )
11 9 10 sylan2 
 |-  ( ( ( F |` ( B i^i dom F ) ) Fn ( B i^i dom F ) /\ B e. Fin ) -> ( F |` ( B i^i dom F ) ) e. Fin )
12 11 ex 
 |-  ( ( F |` ( B i^i dom F ) ) Fn ( B i^i dom F ) -> ( B e. Fin -> ( F |` ( B i^i dom F ) ) e. Fin ) )
13 7 8 12 3syl 
 |-  ( F Fn A -> ( B e. Fin -> ( F |` ( B i^i dom F ) ) e. Fin ) )
14 13 imp 
 |-  ( ( F Fn A /\ B e. Fin ) -> ( F |` ( B i^i dom F ) ) e. Fin )
15 5 14 eqeltrd 
 |-  ( ( F Fn A /\ B e. Fin ) -> ( F |` B ) e. Fin )