Metamath Proof Explorer

Theorem fsuppimp

Description: Implications of a class being a finitely supported function (in relation to a given zero). (Contributed by AV, 26-May-2019)

Ref Expression
Assertion fsuppimp 
|- ( R finSupp Z -> ( Fun R /\ ( R supp Z ) e. Fin ) )

Proof

Step Hyp Ref Expression
1 relfsupp 
 |-  Rel finSupp
2 1 brrelex12i 
 |-  ( R finSupp Z -> ( R e. _V /\ Z e. _V ) )
3 isfsupp 
 |-  ( ( R e. _V /\ Z e. _V ) -> ( R finSupp Z <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
4 3 biimpd 
 |-  ( ( R e. _V /\ Z e. _V ) -> ( R finSupp Z -> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
5 2 4 mpcom 
 |-  ( R finSupp Z -> ( Fun R /\ ( R supp Z ) e. Fin ) )