Metamath Proof Explorer


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 𝑍 )