Metamath Proof Explorer

Theorem fcdmnn0fsupp

Description: A function into NN0 is finitely supported iff its support is finite. (Contributed by AV, 8-Jul-2019)

Ref Expression
Assertion fcdmnn0fsupp 
|- ( ( I e. V /\ F : I --> NN0 ) -> ( F finSupp 0 <-> ( `' F " NN ) e. Fin ) )

Proof

Step Hyp Ref Expression
1 c0ex 
 |-  0 e. _V
2 ffsuppbi 
 |-  ( ( I e. V /\ 0 e. _V ) -> ( F : I --> NN0 -> ( F finSupp 0 <-> ( `' F " ( NN0 \ { 0 } ) ) e. Fin ) ) )
3 1 2 mpan2 
 |-  ( I e. V -> ( F : I --> NN0 -> ( F finSupp 0 <-> ( `' F " ( NN0 \ { 0 } ) ) e. Fin ) ) )
4 3 imp 
 |-  ( ( I e. V /\ F : I --> NN0 ) -> ( F finSupp 0 <-> ( `' F " ( NN0 \ { 0 } ) ) e. Fin ) )
5 dfn2 
 |-  NN = ( NN0 \ { 0 } )
6 5 imaeq2i 
 |-  ( `' F " NN ) = ( `' F " ( NN0 \ { 0 } ) )
7 6 eleq1i 
 |-  ( ( `' F " NN ) e. Fin <-> ( `' F " ( NN0 \ { 0 } ) ) e. Fin )
8 4 7 bitr4di 
 |-  ( ( I e. V /\ F : I --> NN0 ) -> ( F finSupp 0 <-> ( `' F " NN ) e. Fin ) )