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

Metamath Proof Explorer

Theorem elovimad

Description: Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017)

Ref Expression
Hypotheses elovimad.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
elovimad.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
elovimad.3 ⊢ ( 𝜑 → Fun 𝐹 )
elovimad.4 ⊢ ( 𝜑 → ( 𝐶 × 𝐷 ) ⊆ dom 𝐹 )
Assertion elovimad ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 elovimad.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2 elovimad.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
3 elovimad.3 ⊢ ( 𝜑 → Fun 𝐹 )
4 elovimad.4 ⊢ ( 𝜑 → ( 𝐶 × 𝐷 ) ⊆ dom 𝐹 )
5 df-ov ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
6 1 2 opelxpd ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) )
7 4 6 sseldd ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )
8 funfvima ⊢ ( ( Fun 𝐹 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) ) )
9 3 7 8 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) ) )
10 6 9 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) )
11 5 10 eqeltrid ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) )