Metamath Proof Explorer

Theorem ffsrn

Description: The range of a finitely supported function is finite. The proof uses fnrndomnum rather than fnrndomg , and so does not require ax-ac . (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Vincent Gonzalez, 24-Aug-2026)

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 finnum 
 |-  ( ( `' F " ( _V \ { Z } ) ) e. Fin -> ( `' F " ( _V \ { Z } ) ) e. dom card )
31 29 30 syl 
 |-  ( ph -> ( `' F " ( _V \ { Z } ) ) e. dom card )
32 cnvimass 
 |-  ( `' F " ( _V \ { Z } ) ) C_ dom F
33 fores 
 |-  ( ( Fun F /\ ( `' F " ( _V \ { Z } ) ) C_ dom F ) -> ( F |` ( `' F " ( _V \ { Z } ) ) ) : ( `' F " ( _V \ { Z } ) ) -onto-> ( F " ( `' F " ( _V \ { Z } ) ) ) )
34 3 32 33 sylancl 
 |-  ( ph -> ( F |` ( `' F " ( _V \ { Z } ) ) ) : ( `' F " ( _V \ { Z } ) ) -onto-> ( F " ( `' F " ( _V \ { Z } ) ) ) )
35 fofn 
 |-  ( ( F |` ( `' F " ( _V \ { Z } ) ) ) : ( `' F " ( _V \ { Z } ) ) -onto-> ( F " ( `' F " ( _V \ { Z } ) ) ) -> ( F |` ( `' F " ( _V \ { Z } ) ) ) Fn ( `' F " ( _V \ { Z } ) ) )
36 34 35 syl 
 |-  ( ph -> ( F |` ( `' F " ( _V \ { Z } ) ) ) Fn ( `' F " ( _V \ { Z } ) ) )
37 fnrndomnum 
 |-  ( ( `' F " ( _V \ { Z } ) ) e. dom card -> ( ( F |` ( `' F " ( _V \ { Z } ) ) ) Fn ( `' F " ( _V \ { Z } ) ) -> ran ( F |` ( `' F " ( _V \ { Z } ) ) ) ~<_ ( `' F " ( _V \ { Z } ) ) ) )
38 31 36 37 sylc 
 |-  ( ph -> ran ( F |` ( `' F " ( _V \ { Z } ) ) ) ~<_ ( `' F " ( _V \ { Z } ) ) )
39 domfi 
 |-  ( ( ( `' F " ( _V \ { Z } ) ) e. Fin /\ ran ( F |` ( `' F " ( _V \ { Z } ) ) ) ~<_ ( `' F " ( _V \ { Z } ) ) ) -> ran ( F |` ( `' F " ( _V \ { Z } ) ) ) e. Fin )
40 29 38 39 syl2anc 
 |-  ( ph -> ran ( F |` ( `' F " ( _V \ { Z } ) ) ) e. Fin )
41 snfi 
 |-  { Z } e. Fin
42 df-ima 
 |-  ( F " ( `' F " { Z } ) ) = ran ( F |` ( `' F " { Z } ) )
43 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " { Z } ) ) = ( { Z } i^i ran F ) )
44 3 43 syl 
 |-  ( ph -> ( F " ( `' F " { Z } ) ) = ( { Z } i^i ran F ) )
45 42 44 eqtr3id 
 |-  ( ph -> ran ( F |` ( `' F " { Z } ) ) = ( { Z } i^i ran F ) )
46 inss1 
 |-  ( { Z } i^i ran F ) C_ { Z }
47 45 46 eqsstrdi 
 |-  ( ph -> ran ( F |` ( `' F " { Z } ) ) C_ { Z } )
48 ssfi 
 |-  ( ( { Z } e. Fin /\ ran ( F |` ( `' F " { Z } ) ) C_ { Z } ) -> ran ( F |` ( `' F " { Z } ) ) e. Fin )
49 41 47 48 sylancr 
 |-  ( ph -> ran ( F |` ( `' F " { Z } ) ) e. Fin )
50 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 )
51 40 49 50 syl2anc 
 |-  ( ph -> ( ran ( F |` ( `' F " ( _V \ { Z } ) ) ) u. ran ( F |` ( `' F " { Z } ) ) ) e. Fin )
52 26 51 eqeltrd 
 |-  ( ph -> ran F e. Fin )