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 ran F A Fin c 𝒫 B Fin F c = A

Proof

Step Hyp Ref Expression
1 simp3 F Fn B A ran F A Fin A Fin
2 dfss3 A ran F x A x ran F
3 fvelrnb F Fn B x ran F y B F y = x
4 3 ralbidv F Fn B x A x ran F x A y B F y = x
5 2 4 syl5bb F Fn B A ran F x A y B F y = x
6 5 biimpa F Fn B A ran F x A y B F y = x
7 6 3adant3 F Fn B A ran F A Fin x A y B F y = x
8 fveqeq2 y = f x F y = x F f x = x
9 8 ac6sfi A Fin x A y B F y = x f f : A B x A F f x = x
10 1 7 9 syl2anc F Fn B A ran F A Fin f f : A B x A F f x = x
11 fimass f : A B f A B
12 vex f V
13 12 imaex f A V
14 13 elpw f A 𝒫 B f A B
15 11 14 sylibr f : A B f A 𝒫 B
16 15 ad2antrl F Fn B A ran F A Fin f : A B x A F f x = x f A 𝒫 B
17 ffun f : A B Fun f
18 17 ad2antrl F Fn B A ran F A Fin f : A B x A F f x = x Fun f
19 simpl3 F Fn B A ran F A Fin f : A B x A F f x = x A Fin
20 imafi Fun f A Fin f A Fin
21 18 19 20 syl2anc F Fn B A ran F A Fin f : A B x A F f x = x f A Fin
22 16 21 elind F Fn B A ran F A Fin f : A B x A F f x = x f A 𝒫 B Fin
23 fvco3 f : A B x A F f x = F f x
24 fvresi x A I A x = x
25 24 adantl f : A B x A I A x = x
26 23 25 eqeq12d f : A B x A F f x = I A x F f x = x
27 26 ralbidva f : A B x A F f x = I A x x A F f x = x
28 27 biimprd f : A B x A F f x = x x A F f x = I A x
29 28 adantl F Fn B A ran F A Fin f : A B x A F f x = x x A F f x = I A x
30 29 impr F Fn B A ran F A Fin f : A B x A F f x = x x A F f x = I A x
31 simpl1 F Fn B A ran F A Fin f : A B x A F f x = x F Fn B
32 ffn f : A B f Fn A
33 32 ad2antrl F Fn B A ran F A Fin f : A B x A F f x = x f Fn A
34 frn f : A B ran f B
35 34 ad2antrl F Fn B A ran F A Fin f : A B x A F f x = x ran f B
36 fnco F Fn B f Fn A ran f B F f Fn A
37 31 33 35 36 syl3anc F Fn B A ran F A Fin f : A B x A F f x = x F f Fn A
38 fnresi I A Fn A
39 eqfnfv F f Fn A I A Fn A F f = I A x A F f x = I A x
40 37 38 39 sylancl F Fn B A ran F A Fin f : A B x A F f x = x F f = I A x A F f x = I A x
41 30 40 mpbird F Fn B A ran F A Fin f : A B x A F f x = x F f = I A
42 41 imaeq1d F Fn B A ran F A Fin f : A B x A F f x = x F f A = I A A
43 imaco F f A = F f A
44 ssid A A
45 resiima A A I A A = A
46 44 45 ax-mp I A A = A
47 42 43 46 3eqtr3g F Fn B A ran F A Fin f : A B x 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 𝒫 B Fin F f A = A c 𝒫 B Fin F c = A
51 22 47 50 syl2anc F Fn B A ran F A Fin f : A B x A F f x = x c 𝒫 B Fin F c = A
52 10 51 exlimddv F Fn B A ran F A Fin c 𝒫 B Fin F c = A