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

Metamath Proof Explorer

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 )