Metamath Proof Explorer

Theorem frnfsuppbi

Description: Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019)

Ref Expression
Assertion frnfsuppbi 
|- ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> ( F finSupp Z <-> ( `' F " ( S \ { Z } ) ) e. Fin ) ) )

Proof

Step Hyp Ref Expression
1 ffun 
 |-  ( F : I --> S -> Fun F )
2 1 adantl 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> Fun F )
3 fex 
 |-  ( ( F : I --> S /\ I e. V ) -> F e. _V )
4 3 expcom 
 |-  ( I e. V -> ( F : I --> S -> F e. _V ) )
5 4 adantr 
 |-  ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> F e. _V ) )
6 5 imp 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> F e. _V )
7 simplr 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> Z e. W )
8 funisfsupp 
 |-  ( ( Fun F /\ F e. _V /\ Z e. W ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
9 2 6 7 8 syl3anc 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
10 frnsuppeq 
 |-  ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> ( F supp Z ) = ( `' F " ( S \ { Z } ) ) ) )
11 10 imp 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> ( F supp Z ) = ( `' F " ( S \ { Z } ) ) )
12 11 eleq1d 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> ( ( F supp Z ) e. Fin <-> ( `' F " ( S \ { Z } ) ) e. Fin ) )
13 9 12 bitrd 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> ( F finSupp Z <-> ( `' F " ( S \ { Z } ) ) e. Fin ) )
14 13 ex 
 |-  ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> ( F finSupp Z <-> ( `' F " ( S \ { Z } ) ) e. Fin ) ) )