Step |
Hyp |
Ref |
Expression |
1 |
|
c0ex |
|- 0 e. _V |
2 |
|
frnfsuppbi |
|- ( ( 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 ) ) |