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 φ finSupp Z F
fsuppres.z φ Z V
Assertion fsuppres φ finSupp Z F X

Proof

Step Hyp Ref Expression
1 fsuppres.s φ finSupp Z F
2 fsuppres.z φ Z V
3 fsuppimp finSupp Z F Fun F F supp Z Fin
4 relprcnfsupp ¬ F V ¬ finSupp Z F
5 4 con4i finSupp Z F F V
6 1 5 syl φ F V
7 6 2 jca φ F V Z V
8 7 adantr φ Fun F F V Z V
9 ressuppss F V Z V F X supp Z F supp Z
10 ssfi F supp Z Fin F X supp Z F supp Z F X supp Z Fin
11 10 expcom F X supp Z F supp Z F supp Z Fin F X supp Z Fin
12 8 9 11 3syl φ Fun F F supp Z Fin F X supp Z Fin
13 12 expcom Fun F φ F supp Z Fin F X supp Z Fin
14 13 com23 Fun F F supp Z Fin φ F X supp Z Fin
15 14 imp Fun F F supp Z Fin φ F X supp Z Fin
16 3 15 syl finSupp Z F φ F X supp Z Fin
17 1 16 mpcom φ F X supp Z Fin
18 funres Fun F Fun F X
19 18 adantr Fun F F supp Z Fin Fun F X
20 1 3 19 3syl φ Fun F X
21 resexg F V F X V
22 1 5 21 3syl φ F X V
23 funisfsupp Fun F X F X V Z V finSupp Z F X F X supp Z Fin
24 20 22 2 23 syl3anc φ finSupp Z F X F X supp Z Fin
25 17 24 mpbird φ finSupp Z F X