Theorem isfsuppd

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

	Ref	Expression
Hypotheses	isfsuppd.r	$$⊢\phi \to R\in V$$
	isfsuppd.z	$$⊢\phi \to Z\in W$$
	isfsuppd.1	$$⊢\phi \to \mathrm{Fun}R$$
	isfsuppd.2	$$⊢\phi \to R\mathrm{supp}Z\in \mathrm{Fin}$$
Assertion	isfsuppd	$$⊢\phi \to {finSupp}_Z\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfsuppd.r	$$⊢\phi \to R\in V$$
2		isfsuppd.z	$$⊢\phi \to Z\in W$$
3		isfsuppd.1	$$⊢\phi \to \mathrm{Fun}R$$
4		isfsuppd.2	$$⊢\phi \to R\mathrm{supp}Z\in \mathrm{Fin}$$
5		isfsupp	$$⊢\left(R\in V\wedge Z\in W\right)\to \left({finSupp}_Z\left(R\right)\leftrightarrow \left(\mathrm{Fun}R\wedge R\mathrm{supp}Z\in \mathrm{Fin}\right)\right)$$
6	1 2 5	syl2anc	$$⊢\phi \to \left({finSupp}_Z\left(R\right)\leftrightarrow \left(\mathrm{Fun}R\wedge R\mathrm{supp}Z\in \mathrm{Fin}\right)\right)$$
7	3 4 6	mpbir2and	$$⊢\phi \to {finSupp}_Z\left(R\right)$$