Theorem psrbasfsupp

Description: Rewrite a finite support for nonnegative integers : For functions mapping a set I to the nonnegative integers, having finite support can also be written as having a finite preimage of the positive integers. The latter expression is used for example in psrbas , but with the former expression, theorems about finite support can be used more directly. (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypothesis	psrbasfsupp.d	|- D = { f e. ( NN0 ^m I ) | f finSupp 0 }
Assertion	psrbasfsupp	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }

Proof

Step	Hyp	Ref	Expression
1		psrbasfsupp.d	|- D = { f e. ( NN0 ^m I ) | f finSupp 0 }
2		0nn0	|- 0 e. NN0
3		isfsupp	|- ( ( f e. ( NN0 ^m I ) /\ 0 e. NN0 ) -> ( f finSupp 0 <-> ( Fun f /\ ( f supp 0 ) e. Fin ) ) )
4	2 3	mpan2	|- ( f e. ( NN0 ^m I ) -> ( f finSupp 0 <-> ( Fun f /\ ( f supp 0 ) e. Fin ) ) )
5		elmapfun	|- ( f e. ( NN0 ^m I ) -> Fun f )
6	5	biantrurd	|- ( f e. ( NN0 ^m I ) -> ( ( f supp 0 ) e. Fin <-> ( Fun f /\ ( f supp 0 ) e. Fin ) ) )
7		dfn2	|- NN = ( NN0 \ { 0 } )
8	7	ineq2i	|- ( ran f i^i NN ) = ( ran f i^i ( NN0 \ { 0 } ) )
9		incom	|- ( ran f i^i NN ) = ( NN i^i ran f )
10		indif2	|- ( ran f i^i ( NN0 \ { 0 } ) ) = ( ( ran f i^i NN0 ) \ { 0 } )
11	8 9 10	3eqtr3i	|- ( NN i^i ran f ) = ( ( ran f i^i NN0 ) \ { 0 } )
12		elmapi	|- ( f e. ( NN0 ^m I ) -> f : I --> NN0 )
13	12	frnd	|- ( f e. ( NN0 ^m I ) -> ran f C_ NN0 )
14		dfss2	|- ( ran f C_ NN0 <-> ( ran f i^i NN0 ) = ran f )
15	13 14	sylib	|- ( f e. ( NN0 ^m I ) -> ( ran f i^i NN0 ) = ran f )
16	15	difeq1d	|- ( f e. ( NN0 ^m I ) -> ( ( ran f i^i NN0 ) \ { 0 } ) = ( ran f \ { 0 } ) )
17	11 16	eqtrid	|- ( f e. ( NN0 ^m I ) -> ( NN i^i ran f ) = ( ran f \ { 0 } ) )
18	17	imaeq2d	|- ( f e. ( NN0 ^m I ) -> ( `' f " ( NN i^i ran f ) ) = ( `' f " ( ran f \ { 0 } ) ) )
19		fimacnvinrn	|- ( Fun f -> ( `' f " NN ) = ( `' f " ( NN i^i ran f ) ) )
20	5 19	syl	|- ( f e. ( NN0 ^m I ) -> ( `' f " NN ) = ( `' f " ( NN i^i ran f ) ) )
21		id	|- ( f e. ( NN0 ^m I ) -> f e. ( NN0 ^m I ) )
22	2	a1i	|- ( f e. ( NN0 ^m I ) -> 0 e. NN0 )
23		supppreima	|- ( ( Fun f /\ f e. ( NN0 ^m I ) /\ 0 e. NN0 ) -> ( f supp 0 ) = ( `' f " ( ran f \ { 0 } ) ) )
24	5 21 22 23	syl3anc	|- ( f e. ( NN0 ^m I ) -> ( f supp 0 ) = ( `' f " ( ran f \ { 0 } ) ) )
25	18 20 24	3eqtr4rd	|- ( f e. ( NN0 ^m I ) -> ( f supp 0 ) = ( `' f " NN ) )
26	25	eleq1d	|- ( f e. ( NN0 ^m I ) -> ( ( f supp 0 ) e. Fin <-> ( `' f " NN ) e. Fin ) )
27	4 6 26	3bitr2d	|- ( f e. ( NN0 ^m I ) -> ( f finSupp 0 <-> ( `' f " NN ) e. Fin ) )
28	27	rabbiia	|- { f e. ( NN0 ^m I ) | f finSupp 0 } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
29	1 28	eqtri	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }