Metamath Proof Explorer

Theorem fcdmnn0supp

Description: Two ways to write the support of a function into NN0 . (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by AV, 7-Jul-2019)

Ref Expression
Assertion fcdmnn0supp 
|- ( ( I e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )

Proof

Step Hyp Ref Expression
1 c0ex 
 |-  0 e. _V
2 fsuppeq 
 |-  ( ( I e. V /\ 0 e. _V ) -> ( F : I --> NN0 -> ( F supp 0 ) = ( `' F " ( NN0 \ { 0 } ) ) ) )
3 1 2 mpan2 
 |-  ( I e. V -> ( F : I --> NN0 -> ( F supp 0 ) = ( `' F " ( NN0 \ { 0 } ) ) ) )
4 3 imp 
 |-  ( ( I e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " ( NN0 \ { 0 } ) ) )
5 dfn2 
 |-  NN = ( NN0 \ { 0 } )
6 5 imaeq2i 
 |-  ( `' F " NN ) = ( `' F " ( NN0 \ { 0 } ) )
7 4 6 eqtr4di 
 |-  ( ( I e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )