Metamath Proof Explorer

Theorem frnnn0supp

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

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

Proof

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