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 fvres 
 |-  ( B e. A -> ( ( F |` A ) ` B ) = ( F ` B ) )
7 6 eleq1d 
 |-  ( B e. A -> ( ( ( F |` A ) ` B ) e. ran ( F |` A ) <-> ( F ` B ) e. ran ( F |` A ) ) )
8 df-ima 
 |-  ( F " A ) = ran ( F |` A )
9 8 eleq2i 
 |-  ( ( F ` B ) e. ( F " A ) <-> ( F ` B ) e. ran ( F |` A ) )
10 7 9 syl6rbbr 
 |-  ( 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 ) ) )