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 ) |
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 ) |