This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isfsupp

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

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

Proof

Step Hyp Ref Expression
1 funeq 
 |-  ( r = R -> ( Fun r <-> Fun R ) )
2 1 adantr 
 |-  ( ( r = R /\ z = Z ) -> ( Fun r <-> Fun R ) )
3 oveq12 
 |-  ( ( r = R /\ z = Z ) -> ( r supp z ) = ( R supp Z ) )
4 3 eleq1d 
 |-  ( ( r = R /\ z = Z ) -> ( ( r supp z ) e. Fin <-> ( R supp Z ) e. Fin ) )
5 2 4 anbi12d 
 |-  ( ( r = R /\ z = Z ) -> ( ( Fun r /\ ( r supp z ) e. Fin ) <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
6 df-fsupp 
 |-  finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
7 5 6 brabga 
 |-  ( ( R e. V /\ Z e. W ) -> ( R finSupp Z <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )