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 
|- ( ph -> A e. C )
elovimad.2 
|- ( ph -> B e. D )
elovimad.3 
|- ( ph -> Fun F )
elovimad.4 
|- ( ph -> ( C X. D ) C_ dom F )
Assertion elovimad 
|- ( ph -> ( A F B ) e. ( F " ( C X. D ) ) )

Proof

Step Hyp Ref Expression
1 elovimad.1 
 |-  ( ph -> A e. C )
2 elovimad.2 
 |-  ( ph -> B e. D )
3 elovimad.3 
 |-  ( ph -> Fun F )
4 elovimad.4 
 |-  ( ph -> ( C X. D ) C_ dom F )
5 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
6 1 2 opelxpd 
 |-  ( ph -> <. A , B >. e. ( C X. D ) )
7 4 6 sseldd 
 |-  ( ph -> <. A , B >. e. dom F )
8 funfvima 
 |-  ( ( Fun F /\ <. A , B >. e. dom F ) -> ( <. A , B >. e. ( C X. D ) -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) ) )
9 3 7 8 syl2anc 
 |-  ( ph -> ( <. A , B >. e. ( C X. D ) -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) ) )
10 6 9 mpd 
 |-  ( ph -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) )
11 5 10 eqeltrid 
 |-  ( ph -> ( A F B ) e. ( F " ( C X. D ) ) )