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

Metamath Proof Explorer

Theorem resfifsupp

Description: The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019)

Ref Expression
Hypotheses resfifsupp.f 
|- ( ph -> Fun F )
resfifsupp.x 
|- ( ph -> X e. Fin )
resfifsupp.z 
|- ( ph -> Z e. V )
Assertion resfifsupp 
|- ( ph -> ( F |` X ) finSupp Z )

Proof

Step Hyp Ref Expression
1 resfifsupp.f 
 |-  ( ph -> Fun F )
2 resfifsupp.x 
 |-  ( ph -> X e. Fin )
3 resfifsupp.z 
 |-  ( ph -> Z e. V )
4 funrel 
 |-  ( Fun F -> Rel F )
5 1 4 syl 
 |-  ( ph -> Rel F )
6 resindm 
 |-  ( Rel F -> ( F |` ( X i^i dom F ) ) = ( F |` X ) )
7 5 6 syl 
 |-  ( ph -> ( F |` ( X i^i dom F ) ) = ( F |` X ) )
8 1 funfnd 
 |-  ( ph -> F Fn dom F )
9 fnresin2 
 |-  ( F Fn dom F -> ( F |` ( X i^i dom F ) ) Fn ( X i^i dom F ) )
10 8 9 syl 
 |-  ( ph -> ( F |` ( X i^i dom F ) ) Fn ( X i^i dom F ) )
11 infi 
 |-  ( X e. Fin -> ( X i^i dom F ) e. Fin )
12 2 11 syl 
 |-  ( ph -> ( X i^i dom F ) e. Fin )
13 10 12 3 fndmfifsupp 
 |-  ( ph -> ( F |` ( X i^i dom F ) ) finSupp Z )
14 7 13 eqbrtrrd 
 |-  ( ph -> ( F |` X ) finSupp Z )