Theorem isfsuppd

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

	Ref	Expression
Hypotheses	isfsuppd.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	isfsuppd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
	isfsuppd.1	⊢ ( 𝜑 → Fun 𝑅 )
	isfsuppd.2	⊢ ( 𝜑 → ( 𝑅 supp 𝑍 ) ∈ Fin )
Assertion	isfsuppd	⊢ ( 𝜑 → 𝑅 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		isfsuppd.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
2		isfsuppd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
3		isfsuppd.1	⊢ ( 𝜑 → Fun 𝑅 )
4		isfsuppd.2	⊢ ( 𝜑 → ( 𝑅 supp 𝑍 ) ∈ Fin )
5		isfsupp	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
6	1 2 5	syl2anc	⊢ ( 𝜑 → ( 𝑅 finSupp 𝑍 ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
7	3 4 6	mpbir2and	⊢ ( 𝜑 → 𝑅 finSupp 𝑍 )