Metamath Proof Explorer

Theorem imafi

Description: Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion imafi 
|- ( ( Fun F /\ X e. Fin ) -> ( F " X ) e. Fin )

Proof

Step Hyp Ref Expression
1 imadmres 
 |-  ( F " dom ( F |` X ) ) = ( F " X )
2 simpr 
 |-  ( ( Fun F /\ X e. Fin ) -> X e. Fin )
3 dmres 
 |-  dom ( F |` X ) = ( X i^i dom F )
4 inss1 
 |-  ( X i^i dom F ) C_ X
5 3 4 eqsstri 
 |-  dom ( F |` X ) C_ X
6 ssfi 
 |-  ( ( X e. Fin /\ dom ( F |` X ) C_ X ) -> dom ( F |` X ) e. Fin )
7 2 5 6 sylancl 
 |-  ( ( Fun F /\ X e. Fin ) -> dom ( F |` X ) e. Fin )
8 resss 
 |-  ( F |` X ) C_ F
9 dmss 
 |-  ( ( F |` X ) C_ F -> dom ( F |` X ) C_ dom F )
10 8 9 mp1i 
 |-  ( ( Fun F /\ X e. Fin ) -> dom ( F |` X ) C_ dom F )
11 fores 
 |-  ( ( Fun F /\ dom ( F |` X ) C_ dom F ) -> ( F |` dom ( F |` X ) ) : dom ( F |` X ) -onto-> ( F " dom ( F |` X ) ) )
12 10 11 syldan 
 |-  ( ( Fun F /\ X e. Fin ) -> ( F |` dom ( F |` X ) ) : dom ( F |` X ) -onto-> ( F " dom ( F |` X ) ) )
13 fofi 
 |-  ( ( dom ( F |` X ) e. Fin /\ ( F |` dom ( F |` X ) ) : dom ( F |` X ) -onto-> ( F " dom ( F |` X ) ) ) -> ( F " dom ( F |` X ) ) e. Fin )
14 7 12 13 syl2anc 
 |-  ( ( Fun F /\ X e. Fin ) -> ( F " dom ( F |` X ) ) e. Fin )
15 1 14 eqeltrrid 
 |-  ( ( Fun F /\ X e. Fin ) -> ( F " X ) e. Fin )