This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsuppfund

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

Ref Expression
Hypothesis fsuppfund.1 ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
Assertion fsuppfund ( 𝜑 → Fun 𝐹 )

Proof

Step Hyp Ref Expression
1 fsuppfund.1 ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
2 fsuppimp ⊢ ( 𝐹 finSupp 𝑍 → ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
3 2 simpld ⊢ ( 𝐹 finSupp 𝑍 → Fun 𝐹 )
4 1 3 syl ⊢ ( 𝜑 → Fun 𝐹 )