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