Metamath Proof Explorer


Theorem fdmfisuppfi

Description: The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019)

Ref Expression
Hypotheses fdmfisuppfi.f φ F : D R
fdmfisuppfi.d φ D Fin
fdmfisuppfi.z φ Z V
Assertion fdmfisuppfi φ F supp Z Fin

Proof

Step Hyp Ref Expression
1 fdmfisuppfi.f φ F : D R
2 fdmfisuppfi.d φ D Fin
3 fdmfisuppfi.z φ 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