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 ) ) )