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 ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑅 𝑌 ) ∈ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 𝑅 𝑌 ) = ∅ ) → ( 𝑋 𝑅 𝑌 ) = ∅ )
2 ssun2 ⊢ { ∅ } ⊆ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } )
3 0ex ⊢ ∅ ∈ V
4 3 snid ⊢ ∅ ∈ { ∅ }
5 2 4 sselii ⊢ ∅ ∈ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } )
6 1 5 eqeltrdi ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 𝑅 𝑌 ) = ∅ ) → ( 𝑋 𝑅 𝑌 ) ∈ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } ) )
7 ssun1 ⊢ ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ⊆ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } )
8 df-ov ⊢ ( 𝑋 𝑅 𝑌 ) = ( 𝑅 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
9 opelxpi ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
10 8 eqeq1i ⊢ ( ( 𝑋 𝑅 𝑌 ) = ∅ ↔ ( 𝑅 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ∅ )
11 10 notbii ⊢ ( ¬ ( 𝑋 𝑅 𝑌 ) = ∅ ↔ ¬ ( 𝑅 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ∅ )
12 11 biimpi ⊢ ( ¬ ( 𝑋 𝑅 𝑌 ) = ∅ → ¬ ( 𝑅 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ∅ )
13 eliman0 ⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ¬ ( 𝑅 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ∅ ) → ( 𝑅 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ ( 𝑅 “ ( 𝐴 × 𝐵 ) ) )
14 9 12 13 syl2an ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 𝑅 𝑌 ) = ∅ ) → ( 𝑅 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ ( 𝑅 “ ( 𝐴 × 𝐵 ) ) )
15 8 14 eqeltrid ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 𝑅 𝑌 ) = ∅ ) → ( 𝑋 𝑅 𝑌 ) ∈ ( 𝑅 “ ( 𝐴 × 𝐵 ) ) )
16 7 15 sselid ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 𝑅 𝑌 ) = ∅ ) → ( 𝑋 𝑅 𝑌 ) ∈ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } ) )
17 6 16 pm2.61dan ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑅 𝑌 ) ∈ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } ) )