Metamath Proof Explorer

Theorem fsupprnfi

Description: Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024)

Ref Expression
Assertion fsupprnfi 
|- ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> ran F e. Fin )

Proof

Step Hyp Ref Expression
1 snfi 
 |-  { .0. } e. Fin
2 simpll 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> Fun F )
3 simplr 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> F e. V )
4 simprl 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> .0. e. W )
5 ressupprn 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ran ( F |` ( F supp .0. ) ) = ( ran F \ { .0. } ) )
6 2 3 4 5 syl3anc 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> ran ( F |` ( F supp .0. ) ) = ( ran F \ { .0. } ) )
7 simprr 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> F finSupp .0. )
8 7 fsuppimpd 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> ( F supp .0. ) e. Fin )
9 suppssdm 
 |-  ( F supp .0. ) C_ dom F
10 ssdmres 
 |-  ( ( F supp .0. ) C_ dom F <-> dom ( F |` ( F supp .0. ) ) = ( F supp .0. ) )
11 9 10 mpbi 
 |-  dom ( F |` ( F supp .0. ) ) = ( F supp .0. )
12 2 funresd 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> Fun ( F |` ( F supp .0. ) ) )
13 funforn 
 |-  ( Fun ( F |` ( F supp .0. ) ) <-> ( F |` ( F supp .0. ) ) : dom ( F |` ( F supp .0. ) ) -onto-> ran ( F |` ( F supp .0. ) ) )
14 12 13 sylib 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> ( F |` ( F supp .0. ) ) : dom ( F |` ( F supp .0. ) ) -onto-> ran ( F |` ( F supp .0. ) ) )
15 foeq2 
 |-  ( dom ( F |` ( F supp .0. ) ) = ( F supp .0. ) -> ( ( F |` ( F supp .0. ) ) : dom ( F |` ( F supp .0. ) ) -onto-> ran ( F |` ( F supp .0. ) ) <-> ( F |` ( F supp .0. ) ) : ( F supp .0. ) -onto-> ran ( F |` ( F supp .0. ) ) ) )
16 15 biimpa 
 |-  ( ( dom ( F |` ( F supp .0. ) ) = ( F supp .0. ) /\ ( F |` ( F supp .0. ) ) : dom ( F |` ( F supp .0. ) ) -onto-> ran ( F |` ( F supp .0. ) ) ) -> ( F |` ( F supp .0. ) ) : ( F supp .0. ) -onto-> ran ( F |` ( F supp .0. ) ) )
17 11 14 16 sylancr 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> ( F |` ( F supp .0. ) ) : ( F supp .0. ) -onto-> ran ( F |` ( F supp .0. ) ) )
18 fofi 
 |-  ( ( ( F supp .0. ) e. Fin /\ ( F |` ( F supp .0. ) ) : ( F supp .0. ) -onto-> ran ( F |` ( F supp .0. ) ) ) -> ran ( F |` ( F supp .0. ) ) e. Fin )
19 8 17 18 syl2anc 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> ran ( F |` ( F supp .0. ) ) e. Fin )
20 6 19 eqeltrrd 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> ( ran F \ { .0. } ) e. Fin )
21 diffib 
 |-  ( { .0. } e. Fin -> ( ran F e. Fin <-> ( ran F \ { .0. } ) e. Fin ) )
22 21 biimpar 
 |-  ( ( { .0. } e. Fin /\ ( ran F \ { .0. } ) e. Fin ) -> ran F e. Fin )
23 1 20 22 sylancr 
 |-  ( ( ( Fun F /\ F e. V ) /\ ( .0. e. W /\ F finSupp .0. ) ) -> ran F e. Fin )