Metamath Proof Explorer

Theorem f1elima

Description: Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion f1elima 
|- ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( ( F ` X ) e. ( F " Y ) <-> X e. Y ) )

Proof

Step Hyp Ref Expression
1 f1fn 
 |-  ( F : A -1-1-> B -> F Fn A )
2 fvelimab 
 |-  ( ( F Fn A /\ Y C_ A ) -> ( ( F ` X ) e. ( F " Y ) <-> E. z e. Y ( F ` z ) = ( F ` X ) ) )
3 1 2 sylan 
 |-  ( ( F : A -1-1-> B /\ Y C_ A ) -> ( ( F ` X ) e. ( F " Y ) <-> E. z e. Y ( F ` z ) = ( F ` X ) ) )
4 3 3adant2 
 |-  ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( ( F ` X ) e. ( F " Y ) <-> E. z e. Y ( F ` z ) = ( F ` X ) ) )
5 ssel 
 |-  ( Y C_ A -> ( z e. Y -> z e. A ) )
6 5 impac 
 |-  ( ( Y C_ A /\ z e. Y ) -> ( z e. A /\ z e. Y ) )
7 f1fveq 
 |-  ( ( F : A -1-1-> B /\ ( z e. A /\ X e. A ) ) -> ( ( F ` z ) = ( F ` X ) <-> z = X ) )
8 7 ancom2s 
 |-  ( ( F : A -1-1-> B /\ ( X e. A /\ z e. A ) ) -> ( ( F ` z ) = ( F ` X ) <-> z = X ) )
9 8 biimpd 
 |-  ( ( F : A -1-1-> B /\ ( X e. A /\ z e. A ) ) -> ( ( F ` z ) = ( F ` X ) -> z = X ) )
10 9 anassrs 
 |-  ( ( ( F : A -1-1-> B /\ X e. A ) /\ z e. A ) -> ( ( F ` z ) = ( F ` X ) -> z = X ) )
11 eleq1 
 |-  ( z = X -> ( z e. Y <-> X e. Y ) )
12 11 biimpcd 
 |-  ( z e. Y -> ( z = X -> X e. Y ) )
13 10 12 sylan9 
 |-  ( ( ( ( F : A -1-1-> B /\ X e. A ) /\ z e. A ) /\ z e. Y ) -> ( ( F ` z ) = ( F ` X ) -> X e. Y ) )
14 13 anasss 
 |-  ( ( ( F : A -1-1-> B /\ X e. A ) /\ ( z e. A /\ z e. Y ) ) -> ( ( F ` z ) = ( F ` X ) -> X e. Y ) )
15 6 14 sylan2 
 |-  ( ( ( F : A -1-1-> B /\ X e. A ) /\ ( Y C_ A /\ z e. Y ) ) -> ( ( F ` z ) = ( F ` X ) -> X e. Y ) )
16 15 anassrs 
 |-  ( ( ( ( F : A -1-1-> B /\ X e. A ) /\ Y C_ A ) /\ z e. Y ) -> ( ( F ` z ) = ( F ` X ) -> X e. Y ) )
17 16 rexlimdva 
 |-  ( ( ( F : A -1-1-> B /\ X e. A ) /\ Y C_ A ) -> ( E. z e. Y ( F ` z ) = ( F ` X ) -> X e. Y ) )
18 17 3impa 
 |-  ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( E. z e. Y ( F ` z ) = ( F ` X ) -> X e. Y ) )
19 eqid 
 |-  ( F ` X ) = ( F ` X )
20 fveqeq2 
 |-  ( z = X -> ( ( F ` z ) = ( F ` X ) <-> ( F ` X ) = ( F ` X ) ) )
21 20 rspcev 
 |-  ( ( X e. Y /\ ( F ` X ) = ( F ` X ) ) -> E. z e. Y ( F ` z ) = ( F ` X ) )
22 19 21 mpan2 
 |-  ( X e. Y -> E. z e. Y ( F ` z ) = ( F ` X ) )
23 18 22 impbid1 
 |-  ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( E. z e. Y ( F ` z ) = ( F ` X ) <-> X e. Y ) )
24 4 23 bitrd 
 |-  ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( ( F ` X ) e. ( F " Y ) <-> X e. Y ) )