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

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	$⊢ φ \to {finSupp}_{Z} (F)$
	Assertion	fsuppimpd	$⊢ φ \to F supp Z \in Fin$

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