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	$⊢ φ \to {finSupp}_{Z} (F)$
	Assertion	fsuppfund	$⊢ φ \to Fun F$

Step	Hyp	Ref	Expression
1		fsuppfund.1	$⊢ φ \to {finSupp}_{Z} (F)$
2		fsuppimp	$⊢ {finSupp}_{Z} (F) \to (Fun F \land F supp Z \in Fin)$
3	2	simpld	$⊢ {finSupp}_{Z} (F) \to Fun F$
4	1 3	syl	$⊢ φ \to Fun F$