Metamath Proof Explorer


Theorem fsuppimpd

Description: A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019)

Ref Expression
Hypothesis fsuppimpd.f
|- ( ph -> F finSupp Z )
Assertion fsuppimpd
|- ( ph -> ( F supp Z ) e. Fin )

Proof

Step Hyp Ref Expression
1 fsuppimpd.f
 |-  ( ph -> F finSupp Z )
2 fsuppimp
 |-  ( F finSupp Z -> ( Fun F /\ ( F supp Z ) e. Fin ) )
3 2 simprd
 |-  ( F finSupp Z -> ( F supp Z ) e. Fin )
4 1 3 syl
 |-  ( ph -> ( F supp Z ) e. Fin )