This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fcdmnn0fsuppg

Description: Version of fcdmnn0fsupp avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 5-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 ffun 
 |-  ( F : I --> NN0 -> Fun F )
2 simpl 
 |-  ( ( F e. V /\ F : I --> NN0 ) -> F e. V )
3 c0ex 
 |-  0 e. _V
4 funisfsupp 
 |-  ( ( Fun F /\ F e. V /\ 0 e. _V ) -> ( F finSupp 0 <-> ( F supp 0 ) e. Fin ) )
5 3 4 mp3an3 
 |-  ( ( Fun F /\ F e. V ) -> ( F finSupp 0 <-> ( F supp 0 ) e. Fin ) )
6 1 2 5 syl2an2 
 |-  ( ( F e. V /\ F : I --> NN0 ) -> ( F finSupp 0 <-> ( F supp 0 ) e. Fin ) )
7 fcdmnn0suppg 
 |-  ( ( F e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )
8 7 eleq1d 
 |-  ( ( F e. V /\ F : I --> NN0 ) -> ( ( F supp 0 ) e. Fin <-> ( `' F " NN ) e. Fin ) )
9 6 8 bitrd 
 |-  ( ( F e. V /\ F : I --> NN0 ) -> ( F finSupp 0 <-> ( `' F " NN ) e. Fin ) )