Metamath Proof Explorer

Theorem ssimaex

Description: The existence of a subimage. (Contributed by NM, 8-Apr-2007)

Ref Expression
Hypothesis ssimaex.1 
|- A e. _V
Assertion ssimaex 
|- ( ( Fun F /\ B C_ ( F " A ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) )

Proof

Step Hyp Ref Expression
1 ssimaex.1 
 |-  A e. _V
2 dmres 
 |-  dom ( F |` A ) = ( A i^i dom F )
3 2 imaeq2i 
 |-  ( F " dom ( F |` A ) ) = ( F " ( A i^i dom F ) )
4 imadmres 
 |-  ( F " dom ( F |` A ) ) = ( F " A )
5 3 4 eqtr3i 
 |-  ( F " ( A i^i dom F ) ) = ( F " A )
6 5 sseq2i 
 |-  ( B C_ ( F " ( A i^i dom F ) ) <-> B C_ ( F " A ) )
7 ssrab2 
 |-  { y e. ( A i^i dom F ) | ( F ` y ) e. B } C_ ( A i^i dom F )
8 ssel2 
 |-  ( ( B C_ ( F " ( A i^i dom F ) ) /\ z e. B ) -> z e. ( F " ( A i^i dom F ) ) )
9 8 adantll 
 |-  ( ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) /\ z e. B ) -> z e. ( F " ( A i^i dom F ) ) )
10 fvelima 
 |-  ( ( Fun F /\ z e. ( F " ( A i^i dom F ) ) ) -> E. w e. ( A i^i dom F ) ( F ` w ) = z )
11 10 ex 
 |-  ( Fun F -> ( z e. ( F " ( A i^i dom F ) ) -> E. w e. ( A i^i dom F ) ( F ` w ) = z ) )
12 11 adantr 
 |-  ( ( Fun F /\ z e. B ) -> ( z e. ( F " ( A i^i dom F ) ) -> E. w e. ( A i^i dom F ) ( F ` w ) = z ) )
13 eleq1a 
 |-  ( z e. B -> ( ( F ` w ) = z -> ( F ` w ) e. B ) )
14 13 anim2d 
 |-  ( z e. B -> ( ( w e. ( A i^i dom F ) /\ ( F ` w ) = z ) -> ( w e. ( A i^i dom F ) /\ ( F ` w ) e. B ) ) )
15 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
16 15 eleq1d 
 |-  ( y = w -> ( ( F ` y ) e. B <-> ( F ` w ) e. B ) )
17 16 elrab 
 |-  ( w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } <-> ( w e. ( A i^i dom F ) /\ ( F ` w ) e. B ) )
18 14 17 imbitrrdi 
 |-  ( z e. B -> ( ( w e. ( A i^i dom F ) /\ ( F ` w ) = z ) -> w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) )
19 simpr 
 |-  ( ( w e. ( A i^i dom F ) /\ ( F ` w ) = z ) -> ( F ` w ) = z )
20 18 19 jca2 
 |-  ( z e. B -> ( ( w e. ( A i^i dom F ) /\ ( F ` w ) = z ) -> ( w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } /\ ( F ` w ) = z ) ) )
21 20 reximdv2 
 |-  ( z e. B -> ( E. w e. ( A i^i dom F ) ( F ` w ) = z -> E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z ) )
22 21 adantl 
 |-  ( ( Fun F /\ z e. B ) -> ( E. w e. ( A i^i dom F ) ( F ` w ) = z -> E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z ) )
23 funfn 
 |-  ( Fun F <-> F Fn dom F )
24 inss2 
 |-  ( A i^i dom F ) C_ dom F
25 7 24 sstri 
 |-  { y e. ( A i^i dom F ) | ( F ` y ) e. B } C_ dom F
26 fvelimab 
 |-  ( ( F Fn dom F /\ { y e. ( A i^i dom F ) | ( F ` y ) e. B } C_ dom F ) -> ( z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) <-> E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z ) )
27 25 26 mpan2 
 |-  ( F Fn dom F -> ( z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) <-> E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z ) )
28 23 27 sylbi 
 |-  ( Fun F -> ( z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) <-> E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z ) )
29 28 adantr 
 |-  ( ( Fun F /\ z e. B ) -> ( z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) <-> E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z ) )
30 22 29 sylibrd 
 |-  ( ( Fun F /\ z e. B ) -> ( E. w e. ( A i^i dom F ) ( F ` w ) = z -> z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) )
31 12 30 syld 
 |-  ( ( Fun F /\ z e. B ) -> ( z e. ( F " ( A i^i dom F ) ) -> z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) )
32 31 adantlr 
 |-  ( ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) /\ z e. B ) -> ( z e. ( F " ( A i^i dom F ) ) -> z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) )
33 9 32 mpd 
 |-  ( ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) /\ z e. B ) -> z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) )
34 33 ex 
 |-  ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) -> ( z e. B -> z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) )
35 fvelima 
 |-  ( ( Fun F /\ z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) -> E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z )
36 35 ex 
 |-  ( Fun F -> ( z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) -> E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z ) )
37 eleq1 
 |-  ( ( F ` w ) = z -> ( ( F ` w ) e. B <-> z e. B ) )
38 37 biimpcd 
 |-  ( ( F ` w ) e. B -> ( ( F ` w ) = z -> z e. B ) )
39 38 adantl 
 |-  ( ( w e. ( A i^i dom F ) /\ ( F ` w ) e. B ) -> ( ( F ` w ) = z -> z e. B ) )
40 17 39 sylbi 
 |-  ( w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } -> ( ( F ` w ) = z -> z e. B ) )
41 40 rexlimiv 
 |-  ( E. w e. { y e. ( A i^i dom F ) | ( F ` y ) e. B } ( F ` w ) = z -> z e. B )
42 36 41 syl6 
 |-  ( Fun F -> ( z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) -> z e. B ) )
43 42 adantr 
 |-  ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) -> ( z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) -> z e. B ) )
44 34 43 impbid 
 |-  ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) -> ( z e. B <-> z e. ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) )
45 44 eqrdv 
 |-  ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) -> B = ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) )
46 1 inex1 
 |-  ( A i^i dom F ) e. _V
47 46 rabex 
 |-  { y e. ( A i^i dom F ) | ( F ` y ) e. B } e. _V
48 sseq1 
 |-  ( x = { y e. ( A i^i dom F ) | ( F ` y ) e. B } -> ( x C_ ( A i^i dom F ) <-> { y e. ( A i^i dom F ) | ( F ` y ) e. B } C_ ( A i^i dom F ) ) )
49 imaeq2 
 |-  ( x = { y e. ( A i^i dom F ) | ( F ` y ) e. B } -> ( F " x ) = ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) )
50 49 eqeq2d 
 |-  ( x = { y e. ( A i^i dom F ) | ( F ` y ) e. B } -> ( B = ( F " x ) <-> B = ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) )
51 48 50 anbi12d 
 |-  ( x = { y e. ( A i^i dom F ) | ( F ` y ) e. B } -> ( ( x C_ ( A i^i dom F ) /\ B = ( F " x ) ) <-> ( { y e. ( A i^i dom F ) | ( F ` y ) e. B } C_ ( A i^i dom F ) /\ B = ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) ) )
52 47 51 spcev 
 |-  ( ( { y e. ( A i^i dom F ) | ( F ` y ) e. B } C_ ( A i^i dom F ) /\ B = ( F " { y e. ( A i^i dom F ) | ( F ` y ) e. B } ) ) -> E. x ( x C_ ( A i^i dom F ) /\ B = ( F " x ) ) )
53 7 45 52 sylancr 
 |-  ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) -> E. x ( x C_ ( A i^i dom F ) /\ B = ( F " x ) ) )
54 inss1 
 |-  ( A i^i dom F ) C_ A
55 sstr 
 |-  ( ( x C_ ( A i^i dom F ) /\ ( A i^i dom F ) C_ A ) -> x C_ A )
56 54 55 mpan2 
 |-  ( x C_ ( A i^i dom F ) -> x C_ A )
57 56 anim1i 
 |-  ( ( x C_ ( A i^i dom F ) /\ B = ( F " x ) ) -> ( x C_ A /\ B = ( F " x ) ) )
58 57 eximi 
 |-  ( E. x ( x C_ ( A i^i dom F ) /\ B = ( F " x ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) )
59 53 58 syl 
 |-  ( ( Fun F /\ B C_ ( F " ( A i^i dom F ) ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) )
60 6 59 sylan2br 
 |-  ( ( Fun F /\ B C_ ( F " A ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) )