Theorem suppssfifsupp

Description: If the support of a function is a subset of a finite set, the function is finitely supported. (Contributed by AV, 15-Jul-2019)

	Ref	Expression
Assertion	suppssfifsupp	|- ( ( ( G e. V /\ Fun G /\ Z e. W ) /\ ( F e. Fin /\ ( G supp Z ) C_ F ) ) -> G finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		ssfi	|- ( ( F e. Fin /\ ( G supp Z ) C_ F ) -> ( G supp Z ) e. Fin )
2	1	adantl	|- ( ( ( G e. V /\ Fun G /\ Z e. W ) /\ ( F e. Fin /\ ( G supp Z ) C_ F ) ) -> ( G supp Z ) e. Fin )
3		3ancoma	|- ( ( G e. V /\ Fun G /\ Z e. W ) <-> ( Fun G /\ G e. V /\ Z e. W ) )
4	3	biimpi	|- ( ( G e. V /\ Fun G /\ Z e. W ) -> ( Fun G /\ G e. V /\ Z e. W ) )
5	4	adantr	|- ( ( ( G e. V /\ Fun G /\ Z e. W ) /\ ( F e. Fin /\ ( G supp Z ) C_ F ) ) -> ( Fun G /\ G e. V /\ Z e. W ) )
6		funisfsupp	|- ( ( Fun G /\ G e. V /\ Z e. W ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) )
7	5 6	syl	|- ( ( ( G e. V /\ Fun G /\ Z e. W ) /\ ( F e. Fin /\ ( G supp Z ) C_ F ) ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) )
8	2 7	mpbird	|- ( ( ( G e. V /\ Fun G /\ Z e. W ) /\ ( F e. Fin /\ ( G supp Z ) C_ F ) ) -> G finSupp Z )