Metamath Proof Explorer

Theorem imafi

Description: Images of finite sets are finite. For a shorter proof using ax-pow , see imafiALT . (Contributed by Stefan O'Rear, 22-Feb-2015) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 imaeq2 
 |-  ( x = (/) -> ( F " x ) = ( F " (/) ) )
2 1 eleq1d 
 |-  ( x = (/) -> ( ( F " x ) e. Fin <-> ( F " (/) ) e. Fin ) )
3 2 imbi2d 
 |-  ( x = (/) -> ( ( Fun F -> ( F " x ) e. Fin ) <-> ( Fun F -> ( F " (/) ) e. Fin ) ) )
4 imaeq2 
 |-  ( x = y -> ( F " x ) = ( F " y ) )
5 4 eleq1d 
 |-  ( x = y -> ( ( F " x ) e. Fin <-> ( F " y ) e. Fin ) )
6 5 imbi2d 
 |-  ( x = y -> ( ( Fun F -> ( F " x ) e. Fin ) <-> ( Fun F -> ( F " y ) e. Fin ) ) )
7 imaeq2 
 |-  ( x = ( y u. { z } ) -> ( F " x ) = ( F " ( y u. { z } ) ) )
8 7 eleq1d 
 |-  ( x = ( y u. { z } ) -> ( ( F " x ) e. Fin <-> ( F " ( y u. { z } ) ) e. Fin ) )
9 8 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( Fun F -> ( F " x ) e. Fin ) <-> ( Fun F -> ( F " ( y u. { z } ) ) e. Fin ) ) )
10 imaeq2 
 |-  ( x = X -> ( F " x ) = ( F " X ) )
11 10 eleq1d 
 |-  ( x = X -> ( ( F " x ) e. Fin <-> ( F " X ) e. Fin ) )
12 11 imbi2d 
 |-  ( x = X -> ( ( Fun F -> ( F " x ) e. Fin ) <-> ( Fun F -> ( F " X ) e. Fin ) ) )
13 ima0 
 |-  ( F " (/) ) = (/)
14 0fin 
 |-  (/) e. Fin
15 13 14 eqeltri 
 |-  ( F " (/) ) e. Fin
16 15 a1i 
 |-  ( Fun F -> ( F " (/) ) e. Fin )
17 funfn 
 |-  ( Fun F <-> F Fn dom F )
18 fnsnfv 
 |-  ( ( F Fn dom F /\ z e. dom F ) -> { ( F ` z ) } = ( F " { z } ) )
19 17 18 sylanb 
 |-  ( ( Fun F /\ z e. dom F ) -> { ( F ` z ) } = ( F " { z } ) )
20 snfi 
 |-  { ( F ` z ) } e. Fin
21 19 20 eqeltrrdi 
 |-  ( ( Fun F /\ z e. dom F ) -> ( F " { z } ) e. Fin )
22 ndmima 
 |-  ( -. z e. dom F -> ( F " { z } ) = (/) )
23 22 14 eqeltrdi 
 |-  ( -. z e. dom F -> ( F " { z } ) e. Fin )
24 23 adantl 
 |-  ( ( Fun F /\ -. z e. dom F ) -> ( F " { z } ) e. Fin )
25 21 24 pm2.61dan 
 |-  ( Fun F -> ( F " { z } ) e. Fin )
26 imaundi 
 |-  ( F " ( y u. { z } ) ) = ( ( F " y ) u. ( F " { z } ) )
27 unfi 
 |-  ( ( ( F " y ) e. Fin /\ ( F " { z } ) e. Fin ) -> ( ( F " y ) u. ( F " { z } ) ) e. Fin )
28 26 27 eqeltrid 
 |-  ( ( ( F " y ) e. Fin /\ ( F " { z } ) e. Fin ) -> ( F " ( y u. { z } ) ) e. Fin )
29 25 28 sylan2 
 |-  ( ( ( F " y ) e. Fin /\ Fun F ) -> ( F " ( y u. { z } ) ) e. Fin )
30 29 expcom 
 |-  ( Fun F -> ( ( F " y ) e. Fin -> ( F " ( y u. { z } ) ) e. Fin ) )
31 30 a2i 
 |-  ( ( Fun F -> ( F " y ) e. Fin ) -> ( Fun F -> ( F " ( y u. { z } ) ) e. Fin ) )
32 31 a1i 
 |-  ( y e. Fin -> ( ( Fun F -> ( F " y ) e. Fin ) -> ( Fun F -> ( F " ( y u. { z } ) ) e. Fin ) ) )
33 3 6 9 12 16 32 findcard2 
 |-  ( X e. Fin -> ( Fun F -> ( F " X ) e. Fin ) )
34 33 impcom 
 |-  ( ( Fun F /\ X e. Fin ) -> ( F " X ) e. Fin )