Metamath Proof Explorer


Theorem funfvima

Description: A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003)

Ref Expression
Assertion funfvima
|- ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) )

Proof

Step Hyp Ref Expression
1 dmres
 |-  dom ( F |` A ) = ( A i^i dom F )
2 1 elin2
 |-  ( B e. dom ( F |` A ) <-> ( B e. A /\ B e. dom F ) )
3 funres
 |-  ( Fun F -> Fun ( F |` A ) )
4 fvelrn
 |-  ( ( Fun ( F |` A ) /\ B e. dom ( F |` A ) ) -> ( ( F |` A ) ` B ) e. ran ( F |` A ) )
5 3 4 sylan
 |-  ( ( Fun F /\ B e. dom ( F |` A ) ) -> ( ( F |` A ) ` B ) e. ran ( F |` A ) )
6 df-ima
 |-  ( F " A ) = ran ( F |` A )
7 6 eleq2i
 |-  ( ( F ` B ) e. ( F " A ) <-> ( F ` B ) e. ran ( F |` A ) )
8 fvres
 |-  ( B e. A -> ( ( F |` A ) ` B ) = ( F ` B ) )
9 8 eleq1d
 |-  ( B e. A -> ( ( ( F |` A ) ` B ) e. ran ( F |` A ) <-> ( F ` B ) e. ran ( F |` A ) ) )
10 7 9 bitr4id
 |-  ( B e. A -> ( ( F ` B ) e. ( F " A ) <-> ( ( F |` A ) ` B ) e. ran ( F |` A ) ) )
11 5 10 syl5ibrcom
 |-  ( ( Fun F /\ B e. dom ( F |` A ) ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) )
12 11 ex
 |-  ( Fun F -> ( B e. dom ( F |` A ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) )
13 2 12 syl5bir
 |-  ( Fun F -> ( ( B e. A /\ B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) )
14 13 expd
 |-  ( Fun F -> ( B e. A -> ( B e. dom F -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) ) )
15 14 com12
 |-  ( B e. A -> ( Fun F -> ( B e. dom F -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) ) )
16 15 impd
 |-  ( B e. A -> ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) )
17 16 pm2.43b
 |-  ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) )