Theorem fnfvimad

Description: A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	fnfvimad.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	fnfvimad.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	fnfvimad.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
Assertion	fnfvimad	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fnfvimad.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		fnfvimad.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		fnfvimad.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
4		inss2	⊢ ( 𝐴 ∩ 𝐶 ) ⊆ 𝐶
5		imass2	⊢ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐶 → ( 𝐹 “ ( 𝐴 ∩ 𝐶 ) ) ⊆ ( 𝐹 “ 𝐶 ) )
6	4 5	ax-mp	⊢ ( 𝐹 “ ( 𝐴 ∩ 𝐶 ) ) ⊆ ( 𝐹 “ 𝐶 )
7		inss1	⊢ ( 𝐴 ∩ 𝐶 ) ⊆ 𝐴
8	7	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) ⊆ 𝐴 )
9	2 3	elind	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 ∩ 𝐶 ) )
10		fnfvima	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐴 ∩ 𝐶 ) ⊆ 𝐴 ∧ 𝐵 ∈ ( 𝐴 ∩ 𝐶 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝐴 ∩ 𝐶 ) ) )
11	1 8 9 10	syl3anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝐴 ∩ 𝐶 ) ) )
12	6 11	sselid	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐶 ) )