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	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ 𝑓 finSupp 0 }
Assertion	psrbasfsupp	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }

Proof

Step	Hyp	Ref	Expression
1		psrbasfsupp.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ 𝑓 finSupp 0 }
2		0nn0	⊢ 0 ∈ ℕ0
3		isfsupp	⊢ ( ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∧ 0 ∈ ℕ0 ) → ( 𝑓 finSupp 0 ↔ ( Fun 𝑓 ∧ ( 𝑓 supp 0 ) ∈ Fin ) ) )
4	2 3	mpan2	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( 𝑓 finSupp 0 ↔ ( Fun 𝑓 ∧ ( 𝑓 supp 0 ) ∈ Fin ) ) )
5		elmapfun	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → Fun 𝑓 )
6	5	biantrurd	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ( 𝑓 supp 0 ) ∈ Fin ↔ ( Fun 𝑓 ∧ ( 𝑓 supp 0 ) ∈ Fin ) ) )
7		dfn2	⊢ ℕ = ( ℕ0 ∖ { 0 } )
8	7	ineq2i	⊢ ( ran 𝑓 ∩ ℕ ) = ( ran 𝑓 ∩ ( ℕ0 ∖ { 0 } ) )
9		incom	⊢ ( ran 𝑓 ∩ ℕ ) = ( ℕ ∩ ran 𝑓 )
10		indif2	⊢ ( ran 𝑓 ∩ ( ℕ0 ∖ { 0 } ) ) = ( ( ran 𝑓 ∩ ℕ0 ) ∖ { 0 } )
11	8 9 10	3eqtr3i	⊢ ( ℕ ∩ ran 𝑓 ) = ( ( ran 𝑓 ∩ ℕ0 ) ∖ { 0 } )
12		elmapi	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ ℕ0 )
13	12	frnd	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ran 𝑓 ⊆ ℕ0 )
14		dfss2	⊢ ( ran 𝑓 ⊆ ℕ0 ↔ ( ran 𝑓 ∩ ℕ0 ) = ran 𝑓 )
15	13 14	sylib	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ran 𝑓 ∩ ℕ0 ) = ran 𝑓 )
16	15	difeq1d	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ( ran 𝑓 ∩ ℕ0 ) ∖ { 0 } ) = ( ran 𝑓 ∖ { 0 } ) )
17	11 16	eqtrid	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ℕ ∩ ran 𝑓 ) = ( ran 𝑓 ∖ { 0 } ) )
18	17	imaeq2d	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ◡ 𝑓 “ ( ℕ ∩ ran 𝑓 ) ) = ( ◡ 𝑓 “ ( ran 𝑓 ∖ { 0 } ) ) )
19		fimacnvinrn	⊢ ( Fun 𝑓 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝑓 “ ( ℕ ∩ ran 𝑓 ) ) )
20	5 19	syl	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝑓 “ ( ℕ ∩ ran 𝑓 ) ) )
21		id	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) )
22	2	a1i	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → 0 ∈ ℕ0 )
23		supppreima	⊢ ( ( Fun 𝑓 ∧ 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∧ 0 ∈ ℕ0 ) → ( 𝑓 supp 0 ) = ( ◡ 𝑓 “ ( ran 𝑓 ∖ { 0 } ) ) )
24	5 21 22 23	syl3anc	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( 𝑓 supp 0 ) = ( ◡ 𝑓 “ ( ran 𝑓 ∖ { 0 } ) ) )
25	18 20 24	3eqtr4rd	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( 𝑓 supp 0 ) = ( ◡ 𝑓 “ ℕ ) )
26	25	eleq1d	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( ( 𝑓 supp 0 ) ∈ Fin ↔ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) )
27	4 6 26	3bitr2d	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) → ( 𝑓 finSupp 0 ↔ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) )
28	27	rabbiia	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
29	1 28	eqtri	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }