Metamath Proof Explorer

Theorem fipreima

Description: Given a finite subset A of the range of a function, there exists a finite subset of the domain whose image is A . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion fipreima 
|- ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) -> E. c e. ( ~P B i^i Fin ) ( F " c ) = A )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) -> A e. Fin )
2 dfss3 
 |-  ( A C_ ran F <-> A. x e. A x e. ran F )
3 fvelrnb 
 |-  ( F Fn B -> ( x e. ran F <-> E. y e. B ( F ` y ) = x ) )
4 3 ralbidv 
 |-  ( F Fn B -> ( A. x e. A x e. ran F <-> A. x e. A E. y e. B ( F ` y ) = x ) )
5 2 4 bitrid 
 |-  ( F Fn B -> ( A C_ ran F <-> A. x e. A E. y e. B ( F ` y ) = x ) )
6 5 biimpa 
 |-  ( ( F Fn B /\ A C_ ran F ) -> A. x e. A E. y e. B ( F ` y ) = x )
7 6 3adant3 
 |-  ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) -> A. x e. A E. y e. B ( F ` y ) = x )
8 fveqeq2 
 |-  ( y = ( f ` x ) -> ( ( F ` y ) = x <-> ( F ` ( f ` x ) ) = x ) )
9 8 ac6sfi 
 |-  ( ( A e. Fin /\ A. x e. A E. y e. B ( F ` y ) = x ) -> E. f ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) )
10 1 7 9 syl2anc 
 |-  ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) -> E. f ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) )
11 fimass 
 |-  ( f : A --> B -> ( f " A ) C_ B )
12 vex 
 |-  f e. _V
13 12 imaex 
 |-  ( f " A ) e. _V
14 13 elpw 
 |-  ( ( f " A ) e. ~P B <-> ( f " A ) C_ B )
15 11 14 sylibr 
 |-  ( f : A --> B -> ( f " A ) e. ~P B )
16 15 ad2antrl 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ( f " A ) e. ~P B )
17 ffun 
 |-  ( f : A --> B -> Fun f )
18 17 ad2antrl 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> Fun f )
19 simpl3 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> A e. Fin )
20 imafi 
 |-  ( ( Fun f /\ A e. Fin ) -> ( f " A ) e. Fin )
21 18 19 20 syl2anc 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ( f " A ) e. Fin )
22 16 21 elind 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ( f " A ) e. ( ~P B i^i Fin ) )
23 fvco3 
 |-  ( ( f : A --> B /\ x e. A ) -> ( ( F o. f ) ` x ) = ( F ` ( f ` x ) ) )
24 fvresi 
 |-  ( x e. A -> ( ( _I |` A ) ` x ) = x )
25 24 adantl 
 |-  ( ( f : A --> B /\ x e. A ) -> ( ( _I |` A ) ` x ) = x )
26 23 25 eqeq12d 
 |-  ( ( f : A --> B /\ x e. A ) -> ( ( ( F o. f ) ` x ) = ( ( _I |` A ) ` x ) <-> ( F ` ( f ` x ) ) = x ) )
27 26 ralbidva 
 |-  ( f : A --> B -> ( A. x e. A ( ( F o. f ) ` x ) = ( ( _I |` A ) ` x ) <-> A. x e. A ( F ` ( f ` x ) ) = x ) )
28 27 biimprd 
 |-  ( f : A --> B -> ( A. x e. A ( F ` ( f ` x ) ) = x -> A. x e. A ( ( F o. f ) ` x ) = ( ( _I |` A ) ` x ) ) )
29 28 adantl 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ f : A --> B ) -> ( A. x e. A ( F ` ( f ` x ) ) = x -> A. x e. A ( ( F o. f ) ` x ) = ( ( _I |` A ) ` x ) ) )
30 29 impr 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> A. x e. A ( ( F o. f ) ` x ) = ( ( _I |` A ) ` x ) )
31 simpl1 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> F Fn B )
32 ffn 
 |-  ( f : A --> B -> f Fn A )
33 32 ad2antrl 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> f Fn A )
34 frn 
 |-  ( f : A --> B -> ran f C_ B )
35 34 ad2antrl 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ran f C_ B )
36 fnco 
 |-  ( ( F Fn B /\ f Fn A /\ ran f C_ B ) -> ( F o. f ) Fn A )
37 31 33 35 36 syl3anc 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ( F o. f ) Fn A )
38 fnresi 
 |-  ( _I |` A ) Fn A
39 eqfnfv 
 |-  ( ( ( F o. f ) Fn A /\ ( _I |` A ) Fn A ) -> ( ( F o. f ) = ( _I |` A ) <-> A. x e. A ( ( F o. f ) ` x ) = ( ( _I |` A ) ` x ) ) )
40 37 38 39 sylancl 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ( ( F o. f ) = ( _I |` A ) <-> A. x e. A ( ( F o. f ) ` x ) = ( ( _I |` A ) ` x ) ) )
41 30 40 mpbird 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ( F o. f ) = ( _I |` A ) )
42 41 imaeq1d 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ( ( F o. f ) " A ) = ( ( _I |` A ) " A ) )
43 imaco 
 |-  ( ( F o. f ) " A ) = ( F " ( f " A ) )
44 ssid 
 |-  A C_ A
45 resiima 
 |-  ( A C_ A -> ( ( _I |` A ) " A ) = A )
46 44 45 ax-mp 
 |-  ( ( _I |` A ) " A ) = A
47 42 43 46 3eqtr3g 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> ( F " ( f " A ) ) = A )
48 imaeq2 
 |-  ( c = ( f " A ) -> ( F " c ) = ( F " ( f " A ) ) )
49 48 eqeq1d 
 |-  ( c = ( f " A ) -> ( ( F " c ) = A <-> ( F " ( f " A ) ) = A ) )
50 49 rspcev 
 |-  ( ( ( f " A ) e. ( ~P B i^i Fin ) /\ ( F " ( f " A ) ) = A ) -> E. c e. ( ~P B i^i Fin ) ( F " c ) = A )
51 22 47 50 syl2anc 
 |-  ( ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A ( F ` ( f ` x ) ) = x ) ) -> E. c e. ( ~P B i^i Fin ) ( F " c ) = A )
52 10 51 exlimddv 
 |-  ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) -> E. c e. ( ~P B i^i Fin ) ( F " c ) = A )