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

Metamath Proof Explorer

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 }