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

Metamath Proof Explorer

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