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	syl6eqel	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 𝑅 𝑌 ) = ∅ ) → ( 𝑋 𝑅 𝑌 ) ∈ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } ) )
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	sseldi	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 𝑅 𝑌 ) = ∅ ) → ( 𝑋 𝑅 𝑌 ) ∈ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } ) )
17	6 16	pm2.61dan	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑅 𝑌 ) ∈ ( ( 𝑅 “ ( 𝐴 × 𝐵 ) ) ∪ { ∅ } ) )