Metamath Proof Explorer

Theorem fsuppsssupp

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

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( G e. V /\ Fun G ) /\ ( F finSupp Z /\ ( G supp Z ) C_ ( F supp Z ) ) ) -> G e. V )
2 simplr 
 |-  ( ( ( G e. V /\ Fun G ) /\ ( F finSupp Z /\ ( G supp Z ) C_ ( F supp Z ) ) ) -> Fun G )
3 relfsupp 
 |-  Rel finSupp
4 3 brrelex2i 
 |-  ( F finSupp Z -> Z e. _V )
5 4 ad2antrl 
 |-  ( ( ( G e. V /\ Fun G ) /\ ( F finSupp Z /\ ( G supp Z ) C_ ( F supp Z ) ) ) -> Z e. _V )
6 id 
 |-  ( F finSupp Z -> F finSupp Z )
7 6 fsuppimpd 
 |-  ( F finSupp Z -> ( F supp Z ) e. Fin )
8 7 anim1i 
 |-  ( ( F finSupp Z /\ ( G supp Z ) C_ ( F supp Z ) ) -> ( ( F supp Z ) e. Fin /\ ( G supp Z ) C_ ( F supp Z ) ) )
9 8 adantl 
 |-  ( ( ( G e. V /\ Fun G ) /\ ( F finSupp Z /\ ( G supp Z ) C_ ( F supp Z ) ) ) -> ( ( F supp Z ) e. Fin /\ ( G supp Z ) C_ ( F supp Z ) ) )
10 suppssfifsupp 
 |-  ( ( ( G e. V /\ Fun G /\ Z e. _V ) /\ ( ( F supp Z ) e. Fin /\ ( G supp Z ) C_ ( F supp Z ) ) ) -> G finSupp Z )
11 1 2 5 9 10 syl31anc 
 |-  ( ( ( G e. V /\ Fun G ) /\ ( F finSupp Z /\ ( G supp Z ) C_ ( F supp Z ) ) ) -> G finSupp Z )