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 φfinSuppZF
Assertion fsuppimpd φFsuppZFin

Proof

Step Hyp Ref Expression
1 fsuppimpd.f φfinSuppZF
2 fsuppimp finSuppZFFunFFsuppZFin
3 2 simprd finSuppZFFsuppZFin
4 1 3 syl φFsuppZFin