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 𝐹𝐵 ∈ dom 𝐹 ) → ( 𝐵𝐴 → ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 dmres dom ( 𝐹𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
2 1 elin2 ( 𝐵 ∈ dom ( 𝐹𝐴 ) ↔ ( 𝐵𝐴𝐵 ∈ dom 𝐹 ) )
3 funres ( Fun 𝐹 → Fun ( 𝐹𝐴 ) )
4 fvelrn ( ( Fun ( 𝐹𝐴 ) ∧ 𝐵 ∈ dom ( 𝐹𝐴 ) ) → ( ( 𝐹𝐴 ) ‘ 𝐵 ) ∈ ran ( 𝐹𝐴 ) )
5 3 4 sylan ( ( Fun 𝐹𝐵 ∈ dom ( 𝐹𝐴 ) ) → ( ( 𝐹𝐴 ) ‘ 𝐵 ) ∈ ran ( 𝐹𝐴 ) )
6 df-ima ( 𝐹𝐴 ) = ran ( 𝐹𝐴 )
7 6 eleq2i ( ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ↔ ( 𝐹𝐵 ) ∈ ran ( 𝐹𝐴 ) )
8 fvres ( 𝐵𝐴 → ( ( 𝐹𝐴 ) ‘ 𝐵 ) = ( 𝐹𝐵 ) )
9 8 eleq1d ( 𝐵𝐴 → ( ( ( 𝐹𝐴 ) ‘ 𝐵 ) ∈ ran ( 𝐹𝐴 ) ↔ ( 𝐹𝐵 ) ∈ ran ( 𝐹𝐴 ) ) )
10 7 9 bitr4id ( 𝐵𝐴 → ( ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ↔ ( ( 𝐹𝐴 ) ‘ 𝐵 ) ∈ ran ( 𝐹𝐴 ) ) )
11 5 10 syl5ibrcom ( ( Fun 𝐹𝐵 ∈ dom ( 𝐹𝐴 ) ) → ( 𝐵𝐴 → ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ) )
12 11 ex ( Fun 𝐹 → ( 𝐵 ∈ dom ( 𝐹𝐴 ) → ( 𝐵𝐴 → ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ) ) )
13 2 12 syl5bir ( Fun 𝐹 → ( ( 𝐵𝐴𝐵 ∈ dom 𝐹 ) → ( 𝐵𝐴 → ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ) ) )
14 13 expd ( Fun 𝐹 → ( 𝐵𝐴 → ( 𝐵 ∈ dom 𝐹 → ( 𝐵𝐴 → ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ) ) ) )
15 14 com12 ( 𝐵𝐴 → ( Fun 𝐹 → ( 𝐵 ∈ dom 𝐹 → ( 𝐵𝐴 → ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ) ) ) )
16 15 impd ( 𝐵𝐴 → ( ( Fun 𝐹𝐵 ∈ dom 𝐹 ) → ( 𝐵𝐴 → ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ) ) )
17 16 pm2.43b ( ( Fun 𝐹𝐵 ∈ dom 𝐹 ) → ( 𝐵𝐴 → ( 𝐹𝐵 ) ∈ ( 𝐹𝐴 ) ) )