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