Theorem frnnn0fsuppg

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

	Ref	Expression
Assertion	frnnn0fsuppg	|- ( ( 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		frnnn0suppg	|- ( ( 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 ) )