This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrid ⊢ ( Fun 𝐹 → ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) ) )
14 13 expd ⊢ ( Fun 𝐹 → ( 𝐵 ∈ 𝐴 → ( 𝐵 ∈ dom 𝐹 → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) ) ) )
15 14 com12 ⊢ ( 𝐵 ∈ 𝐴 → ( Fun 𝐹 → ( 𝐵 ∈ dom 𝐹 → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) ) ) )
16 15 impd ⊢ ( 𝐵 ∈ 𝐴 → ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) ) )
17 16 pm2.43b ⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) )