Metamath Proof Explorer


Theorem fidmfisupp

Description: A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses fidmfisupp.1 φ F : D R
fidmfisupp.2 φ D Fin
fidmfisupp.3 φ Z V
Assertion fidmfisupp φ finSupp Z F

Proof

Step Hyp Ref Expression
1 fidmfisupp.1 φ F : D R
2 fidmfisupp.2 φ D Fin
3 fidmfisupp.3 φ Z V
4 1 2 fexd φ F V
5 suppimacnv F V Z V F supp Z = F -1 V Z
6 4 3 5 syl2anc φ F supp Z = F -1 V Z
7 2 1 fisuppfi φ F -1 V Z Fin
8 6 7 eqeltrd φ F supp Z Fin
9 1 ffund φ Fun F
10 funisfsupp Fun F F V Z V finSupp Z F F supp Z Fin
11 9 4 3 10 syl3anc φ finSupp Z F F supp Z Fin
12 8 11 mpbird φ finSupp Z F