Metamath Proof Explorer

Theorem funisfsupp

Description: The property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019)

Ref Expression
Assertion funisfsupp 
|- ( ( Fun R /\ R e. V /\ Z e. W ) -> ( R finSupp Z <-> ( R supp Z ) e. Fin ) )

Proof

Step Hyp Ref Expression
1 isfsupp 
 |-  ( ( R e. V /\ Z e. W ) -> ( R finSupp Z <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
2 1 3adant1 
 |-  ( ( Fun R /\ R e. V /\ Z e. W ) -> ( R finSupp Z <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
3 ibar 
 |-  ( Fun R -> ( ( R supp Z ) e. Fin <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
4 3 bicomd 
 |-  ( Fun R -> ( ( Fun R /\ ( R supp Z ) e. Fin ) <-> ( R supp Z ) e. Fin ) )
5 4 3ad2ant1 
 |-  ( ( Fun R /\ R e. V /\ Z e. W ) -> ( ( Fun R /\ ( R supp Z ) e. Fin ) <-> ( R supp Z ) e. Fin ) )
6 2 5 bitrd 
 |-  ( ( Fun R /\ R e. V /\ Z e. W ) -> ( R finSupp Z <-> ( R supp Z ) e. Fin ) )