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 \in A \land Y \in B) \to X R Y \in (R [A \times B] \cup \{\emptyset\})$

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((X \in A \land Y \in B) \land X R Y = \emptyset) \to X R Y = \emptyset$
2		ssun2	$⊢ \{\emptyset\} \subseteq R [A \times B] \cup \{\emptyset\}$
3		0ex	$⊢ \emptyset \in V$
4	3	snid	$⊢ \emptyset \in \{\emptyset\}$
5	2 4	sselii	$⊢ \emptyset \in (R [A \times B] \cup \{\emptyset\})$
6	1 5	eqeltrdi	$⊢ ((X \in A \land Y \in B) \land X R Y = \emptyset) \to X R Y \in (R [A \times B] \cup \{\emptyset\})$
7		ssun1	$⊢ R [A \times B] \subseteq R [A \times B] \cup \{\emptyset\}$
8		df-ov	$⊢ X R Y = R (⟨X, Y⟩)$
9		opelxpi	$⊢ (X \in A \land Y \in B) \to ⟨X, Y⟩ \in (A \times B)$
10	8	eqeq1i	$⊢ X R Y = \emptyset \leftrightarrow R (⟨X, Y⟩) = \emptyset$
11	10	notbii	$⊢ \neg X R Y = \emptyset \leftrightarrow \neg R (⟨X, Y⟩) = \emptyset$
12	11	biimpi	$⊢ \neg X R Y = \emptyset \to \neg R (⟨X, Y⟩) = \emptyset$
13		eliman0	$⊢ (⟨X, Y⟩ \in (A \times B) \land \neg R (⟨X, Y⟩) = \emptyset) \to R (⟨X, Y⟩) \in R [A \times B]$
14	9 12 13	syl2an	$⊢ ((X \in A \land Y \in B) \land \neg X R Y = \emptyset) \to R (⟨X, Y⟩) \in R [A \times B]$
15	8 14	eqeltrid	$⊢ ((X \in A \land Y \in B) \land \neg X R Y = \emptyset) \to X R Y \in R [A \times B]$
16	7 15	sselid	$⊢ ((X \in A \land Y \in B) \land \neg X R Y = \emptyset) \to X R Y \in (R [A \times B] \cup \{\emptyset\})$
17	6 16	pm2.61dan	$⊢ (X \in A \land Y \in B) \to X R Y \in (R [A \times B] \cup \{\emptyset\})$

Metamath Proof Explorer