Theorem isfsuppd

Description: Deduction form of isfsupp . (Contributed by SN, 29-Jul-2024)

	Ref	Expression
Hypotheses	isfsuppd.r	|- ( ph -> R e. V )
	isfsuppd.z	|- ( ph -> Z e. W )
	isfsuppd.1	|- ( ph -> Fun R )
	isfsuppd.2	|- ( ph -> ( R supp Z ) e. Fin )
Assertion	isfsuppd	|- ( ph -> R finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		isfsuppd.r	|- ( ph -> R e. V )
2		isfsuppd.z	|- ( ph -> Z e. W )
3		isfsuppd.1	|- ( ph -> Fun R )
4		isfsuppd.2	|- ( ph -> ( R supp Z ) e. Fin )
5		isfsupp	|- ( ( R e. V /\ Z e. W ) -> ( R finSupp Z <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
6	1 2 5	syl2anc	|- ( ph -> ( R finSupp Z <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
7	3 4 6	mpbir2and	|- ( ph -> R finSupp Z )