Metamath Proof Explorer

Theorem ffsrn

Description: The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017)

Ref Expression
Hypotheses ffsrn.z 
|- ( ph -> Z e. W )
ffsrn.0 
|- ( ph -> F e. V )
ffsrn.1 
|- ( ph -> Fun F )
ffsrn.2 
|- ( ph -> ( F supp Z ) e. Fin )
Assertion ffsrn 
|- ( ph -> ran F e. Fin )

Proof

Step Hyp Ref Expression
1 ffsrn.z 
 |-  ( ph -> Z e. W )
2 ffsrn.0 
 |-  ( ph -> F e. V )
3 ffsrn.1 
 |-  ( ph -> Fun F )
4 ffsrn.2 
 |-  ( ph -> ( F supp Z ) e. Fin )
5 dfdm4 
 |-  dom F = ran `' F
6 dfrn4 
 |-  ran `' F = ( `' F " _V )
7 5 6 eqtri 
 |-  dom F = ( `' F " _V )
8 df-fn 
 |-  ( F Fn ( `' F " _V ) <-> ( Fun F /\ dom F = ( `' F " _V ) ) )
9 fnresdm 
 |-  ( F Fn ( `' F " _V ) -> ( F |` ( `' F " _V ) ) = F )
10 8 9 sylbir 
 |-  ( ( Fun F /\ dom F = ( `' F " _V ) ) -> ( F |` ( `' F " _V ) ) = F )
11 3 7 10 sylancl 
 |-  ( ph -> ( F |` ( `' F " _V ) ) = F )
12 imaundi 
 |-  ( `' F " ( ( _V \ { Z } ) u. { Z } ) ) = ( ( `' F " ( _V \ { Z } ) ) u. ( `' F " { Z } ) )
13 12 reseq2i 
 |-  ( F |` ( `' F " ( ( _V \ { Z } ) u. { Z } ) ) ) = ( F |` ( ( `' F " ( _V \ { Z } ) ) u. ( `' F " { Z } ) ) )
14 undif1 
 |-  ( ( _V \ { Z } ) u. { Z } ) = ( _V u. { Z } )
15 ssv 
 |-  { Z } C_ _V
16 ssequn2 
 |-  ( { Z } C_ _V <-> ( _V u. { Z } ) = _V )
17 15 16 mpbi 
 |-  ( _V u. { Z } ) = _V
18 14 17 eqtri 
 |-  ( ( _V \ { Z } ) u. { Z } ) = _V
19 18 imaeq2i 
 |-  ( `' F " ( ( _V \ { Z } ) u. { Z } ) ) = ( `' F " _V )
20 19 reseq2i 
 |-  ( F |` ( `' F " ( ( _V \ { Z } ) u. { Z } ) ) ) = ( F |` ( `' F " _V ) )
21 resundi 
 |-  ( F |` ( ( `' F " ( _V \ { Z } ) ) u. ( `' F " { Z } ) ) ) = ( ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ( F |` ( `' F " { Z } ) ) )
22 13 20 21 3eqtr3i 
 |-  ( F |` ( `' F " _V ) ) = ( ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ( F |` ( `' F " { Z } ) ) )
23 11 22 eqtr3di 
 |-  ( ph -> F = ( ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ( F |` ( `' F " { Z } ) ) ) )
24 23 rneqd 
 |-  ( ph -> ran F = ran ( ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ( F |` ( `' F " { Z } ) ) ) )
25 rnun 
 |-  ran ( ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ( F |` ( `' F " { Z } ) ) ) = ( ran ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ran ( F |` ( `' F " { Z } ) ) )
26 24 25 eqtrdi 
 |-  ( ph -> ran F = ( ran ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ran ( F |` ( `' F " { Z } ) ) ) )
27 suppimacnv 
 |-  ( ( F e. V /\ Z e. W ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
28 2 1 27 syl2anc 
 |-  ( ph -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
29 28 4 eqeltrrd 
 |-  ( ph -> ( `' F " ( _V \ { Z } ) ) e. Fin )
30 cnvexg 
 |-  ( F e. V -> `' F e. _V )
31 imaexg 
 |-  ( `' F e. _V -> ( `' F " ( _V \ { Z } ) ) e. _V )
32 2 30 31 3syl 
 |-  ( ph -> ( `' F " ( _V \ { Z } ) ) e. _V )
33 cnvimass 
 |-  ( `' F " ( _V \ { Z } ) ) C_ dom F
34 fores 
 |-  ( ( Fun F /\ ( `' F " ( _V \ { Z } ) ) C_ dom F ) -> ( F |` ( `' F " ( _V \ { Z } ) ) ) : ( `' F " ( _V \ { Z } ) ) -onto-> ( F " ( `' F " ( _V \ { Z } ) ) ) )
35 3 33 34 sylancl 
 |-  ( ph -> ( F |` ( `' F " ( _V \ { Z } ) ) ) : ( `' F " ( _V \ { Z } ) ) -onto-> ( F " ( `' F " ( _V \ { Z } ) ) ) )
36 fofn 
 |-  ( ( F |` ( `' F " ( _V \ { Z } ) ) ) : ( `' F " ( _V \ { Z } ) ) -onto-> ( F " ( `' F " ( _V \ { Z } ) ) ) -> ( F |` ( `' F " ( _V \ { Z } ) ) ) Fn ( `' F " ( _V \ { Z } ) ) )
37 35 36 syl 
 |-  ( ph -> ( F |` ( `' F " ( _V \ { Z } ) ) ) Fn ( `' F " ( _V \ { Z } ) ) )
38 fnrndomg 
 |-  ( ( `' F " ( _V \ { Z } ) ) e. _V -> ( ( F |` ( `' F " ( _V \ { Z } ) ) ) Fn ( `' F " ( _V \ { Z } ) ) -> ran ( F |` ( `' F " ( _V \ { Z } ) ) ) ~<_ ( `' F " ( _V \ { Z } ) ) ) )
39 32 37 38 sylc 
 |-  ( ph -> ran ( F |` ( `' F " ( _V \ { Z } ) ) ) ~<_ ( `' F " ( _V \ { Z } ) ) )
40 domfi 
 |-  ( ( ( `' F " ( _V \ { Z } ) ) e. Fin /\ ran ( F |` ( `' F " ( _V \ { Z } ) ) ) ~<_ ( `' F " ( _V \ { Z } ) ) ) -> ran ( F |` ( `' F " ( _V \ { Z } ) ) ) e. Fin )
41 29 39 40 syl2anc 
 |-  ( ph -> ran ( F |` ( `' F " ( _V \ { Z } ) ) ) e. Fin )
42 snfi 
 |-  { Z } e. Fin
43 df-ima 
 |-  ( F " ( `' F " { Z } ) ) = ran ( F |` ( `' F " { Z } ) )
44 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " { Z } ) ) = ( { Z } i^i ran F ) )
45 3 44 syl 
 |-  ( ph -> ( F " ( `' F " { Z } ) ) = ( { Z } i^i ran F ) )
46 43 45 eqtr3id 
 |-  ( ph -> ran ( F |` ( `' F " { Z } ) ) = ( { Z } i^i ran F ) )
47 inss1 
 |-  ( { Z } i^i ran F ) C_ { Z }
48 46 47 eqsstrdi 
 |-  ( ph -> ran ( F |` ( `' F " { Z } ) ) C_ { Z } )
49 ssfi 
 |-  ( ( { Z } e. Fin /\ ran ( F |` ( `' F " { Z } ) ) C_ { Z } ) -> ran ( F |` ( `' F " { Z } ) ) e. Fin )
50 42 48 49 sylancr 
 |-  ( ph -> ran ( F |` ( `' F " { Z } ) ) e. Fin )
51 unfi 
 |-  ( ( ran ( F |` ( `' F " ( _V \ { Z } ) ) ) e. Fin /\ ran ( F |` ( `' F " { Z } ) ) e. Fin ) -> ( ran ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ran ( F |` ( `' F " { Z } ) ) ) e. Fin )
52 41 50 51 syl2anc 
 |-  ( ph -> ( ran ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ran ( F |` ( `' F " { Z } ) ) ) e. Fin )
53 26 52 eqeltrd 
 |-  ( ph -> ran F e. Fin )