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 GVFunGZWFFinGsuppZFfinSuppZG

Proof

Step Hyp Ref Expression
1 ssfi FFinGsuppZFGsuppZFin
2 1 adantl GVFunGZWFFinGsuppZFGsuppZFin
3 3ancoma GVFunGZWFunGGVZW
4 3 biimpi GVFunGZWFunGGVZW
5 4 adantr GVFunGZWFFinGsuppZFFunGGVZW
6 funisfsupp FunGGVZWfinSuppZGGsuppZFin
7 5 6 syl GVFunGZWFFinGsuppZFfinSuppZGGsuppZFin
8 2 7 mpbird GVFunGZWFFinGsuppZFfinSuppZG