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 )