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

Metamath Proof Explorer

Theorem fsuppres

Description: The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019)

Ref Expression
Hypotheses fsuppres.s 
|- ( ph -> F finSupp Z )
fsuppres.z 
|- ( ph -> Z e. V )
Assertion fsuppres 
|- ( ph -> ( F |` X ) finSupp Z )

Proof

Step Hyp Ref Expression
1 fsuppres.s 
 |-  ( ph -> F finSupp Z )
2 fsuppres.z 
 |-  ( ph -> Z e. V )
3 fsuppimp 
 |-  ( F finSupp Z -> ( Fun F /\ ( F supp Z ) e. Fin ) )
4 relprcnfsupp 
 |-  ( -. F e. _V -> -. F finSupp Z )
5 4 con4i 
 |-  ( F finSupp Z -> F e. _V )
6 1 5 syl 
 |-  ( ph -> F e. _V )
7 6 2 jca 
 |-  ( ph -> ( F e. _V /\ Z e. V ) )
8 7 adantr 
 |-  ( ( ph /\ Fun F ) -> ( F e. _V /\ Z e. V ) )
9 ressuppss 
 |-  ( ( F e. _V /\ Z e. V ) -> ( ( F |` X ) supp Z ) C_ ( F supp Z ) )
10 ssfi 
 |-  ( ( ( F supp Z ) e. Fin /\ ( ( F |` X ) supp Z ) C_ ( F supp Z ) ) -> ( ( F |` X ) supp Z ) e. Fin )
11 10 expcom 
 |-  ( ( ( F |` X ) supp Z ) C_ ( F supp Z ) -> ( ( F supp Z ) e. Fin -> ( ( F |` X ) supp Z ) e. Fin ) )
12 8 9 11 3syl 
 |-  ( ( ph /\ Fun F ) -> ( ( F supp Z ) e. Fin -> ( ( F |` X ) supp Z ) e. Fin ) )
13 12 expcom 
 |-  ( Fun F -> ( ph -> ( ( F supp Z ) e. Fin -> ( ( F |` X ) supp Z ) e. Fin ) ) )
14 13 com23 
 |-  ( Fun F -> ( ( F supp Z ) e. Fin -> ( ph -> ( ( F |` X ) supp Z ) e. Fin ) ) )
15 14 imp 
 |-  ( ( Fun F /\ ( F supp Z ) e. Fin ) -> ( ph -> ( ( F |` X ) supp Z ) e. Fin ) )
16 3 15 syl 
 |-  ( F finSupp Z -> ( ph -> ( ( F |` X ) supp Z ) e. Fin ) )
17 1 16 mpcom 
 |-  ( ph -> ( ( F |` X ) supp Z ) e. Fin )
18 funres 
 |-  ( Fun F -> Fun ( F |` X ) )
19 18 adantr 
 |-  ( ( Fun F /\ ( F supp Z ) e. Fin ) -> Fun ( F |` X ) )
20 1 3 19 3syl 
 |-  ( ph -> Fun ( F |` X ) )
21 resexg 
 |-  ( F e. _V -> ( F |` X ) e. _V )
22 1 5 21 3syl 
 |-  ( ph -> ( F |` X ) e. _V )
23 funisfsupp 
 |-  ( ( Fun ( F |` X ) /\ ( F |` X ) e. _V /\ Z e. V ) -> ( ( F |` X ) finSupp Z <-> ( ( F |` X ) supp Z ) e. Fin ) )
24 20 22 2 23 syl3anc 
 |-  ( ph -> ( ( F |` X ) finSupp Z <-> ( ( F |` X ) supp Z ) e. Fin ) )
25 17 24 mpbird 
 |-  ( ph -> ( F |` X ) finSupp Z )