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

Metamath Proof Explorer

Theorem ovima0

Description: An operation value is a member of the image plus null. (Contributed by Thierry Arnoux, 25-Jun-2019)

Ref Expression
Assertion ovima0 
|- ( ( X e. A /\ Y e. B ) -> ( X R Y ) e. ( ( R " ( A X. B ) ) u. { (/) } ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( X e. A /\ Y e. B ) /\ ( X R Y ) = (/) ) -> ( X R Y ) = (/) )
2 ssun2 
 |-  { (/) } C_ ( ( R " ( A X. B ) ) u. { (/) } )
3 0ex 
 |-  (/) e. _V
4 3 snid 
 |-  (/) e. { (/) }
5 2 4 sselii 
 |-  (/) e. ( ( R " ( A X. B ) ) u. { (/) } )
6 1 5 eqeltrdi 
 |-  ( ( ( X e. A /\ Y e. B ) /\ ( X R Y ) = (/) ) -> ( X R Y ) e. ( ( R " ( A X. B ) ) u. { (/) } ) )
7 ssun1 
 |-  ( R " ( A X. B ) ) C_ ( ( R " ( A X. B ) ) u. { (/) } )
8 df-ov 
 |-  ( X R Y ) = ( R ` <. X , Y >. )
9 opelxpi 
 |-  ( ( X e. A /\ Y e. B ) -> <. X , Y >. e. ( A X. B ) )
10 8 eqeq1i 
 |-  ( ( X R Y ) = (/) <-> ( R ` <. X , Y >. ) = (/) )
11 10 notbii 
 |-  ( -. ( X R Y ) = (/) <-> -. ( R ` <. X , Y >. ) = (/) )
12 11 biimpi 
 |-  ( -. ( X R Y ) = (/) -> -. ( R ` <. X , Y >. ) = (/) )
13 eliman0 
 |-  ( ( <. X , Y >. e. ( A X. B ) /\ -. ( R ` <. X , Y >. ) = (/) ) -> ( R ` <. X , Y >. ) e. ( R " ( A X. B ) ) )
14 9 12 13 syl2an 
 |-  ( ( ( X e. A /\ Y e. B ) /\ -. ( X R Y ) = (/) ) -> ( R ` <. X , Y >. ) e. ( R " ( A X. B ) ) )
15 8 14 eqeltrid 
 |-  ( ( ( X e. A /\ Y e. B ) /\ -. ( X R Y ) = (/) ) -> ( X R Y ) e. ( R " ( A X. B ) ) )
16 7 15 sselid 
 |-  ( ( ( X e. A /\ Y e. B ) /\ -. ( X R Y ) = (/) ) -> ( X R Y ) e. ( ( R " ( A X. B ) ) u. { (/) } ) )
17 6 16 pm2.61dan 
 |-  ( ( X e. A /\ Y e. B ) -> ( X R Y ) e. ( ( R " ( A X. B ) ) u. { (/) } ) )