Metamath Proof Explorer

Theorem elpreima

Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion elpreima 
|- ( F Fn A -> ( B e. ( `' F " C ) <-> ( B e. A /\ ( F ` B ) e. C ) ) )

Proof

Step Hyp Ref Expression
1 cnvimass 
 |-  ( `' F " C ) C_ dom F
2 1 sseli 
 |-  ( B e. ( `' F " C ) -> B e. dom F )
3 fndm 
 |-  ( F Fn A -> dom F = A )
4 3 eleq2d 
 |-  ( F Fn A -> ( B e. dom F <-> B e. A ) )
5 2 4 syl5ib 
 |-  ( F Fn A -> ( B e. ( `' F " C ) -> B e. A ) )
6 fnfun 
 |-  ( F Fn A -> Fun F )
7 fvimacnvi 
 |-  ( ( Fun F /\ B e. ( `' F " C ) ) -> ( F ` B ) e. C )
8 6 7 sylan 
 |-  ( ( F Fn A /\ B e. ( `' F " C ) ) -> ( F ` B ) e. C )
9 8 ex 
 |-  ( F Fn A -> ( B e. ( `' F " C ) -> ( F ` B ) e. C ) )
10 5 9 jcad 
 |-  ( F Fn A -> ( B e. ( `' F " C ) -> ( B e. A /\ ( F ` B ) e. C ) ) )
11 fvimacnv 
 |-  ( ( Fun F /\ B e. dom F ) -> ( ( F ` B ) e. C <-> B e. ( `' F " C ) ) )
12 11 funfni 
 |-  ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) e. C <-> B e. ( `' F " C ) ) )
13 12 biimpd 
 |-  ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) e. C -> B e. ( `' F " C ) ) )
14 13 expimpd 
 |-  ( F Fn A -> ( ( B e. A /\ ( F ` B ) e. C ) -> B e. ( `' F " C ) ) )
15 10 14 impbid 
 |-  ( F Fn A -> ( B e. ( `' F " C ) <-> ( B e. A /\ ( F ` B ) e. C ) ) )