Metamath Proof Explorer

Theorem fsuppfund

Description: A finitely supported function is a function. (Contributed by SN, 8-Mar-2025)

Ref Expression
Hypothesis fsuppfund.1 
|- ( ph -> F finSupp Z )
Assertion fsuppfund 
|- ( ph -> Fun F )

Proof

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