logically prove: $R$ is Relation $\to R\subseteq\operatorname{dom}(R)\times \operatorname{cod}(R)$

Question

I must logically prove following (with $R$ set or class):

$R$ is Relation $\to R\subseteq\operatorname{dom}(R)\times \operatorname{cod}(R)$

Definitions:

$R$ is Relation if $\forall x \in R: \exists y,z: x=(y,z)$

$\operatorname{dom}(R):=\{x|\exists y:(x,y)\in R\}$

$\operatorname{cod}(R):=\{x|\exists y:(y,x)\in R\}$

UPDATE: I thinked following:

$$\begin{align}x\in R &\leftrightarrow\exists y:\exists z:x=(y,z)\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge (y,z)\in R \wedge (y,z)\in R\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge\exists z:(y,z)\in R\wedge\exists z:(y,z)\in R\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge\exists y:\exists z:(y,z)\in R\wedge\exists y:\exists z:(y,z)\in R\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge\exists y:y\in\operatorname{dom}(R)\wedge\exists z:\exists y:(y,z)\in R\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge\exists y:y\in\operatorname{dom}(R)\wedge \exists z:z\in \operatorname{cod}(R)\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge z\in\operatorname{cod}(R)\wedge\exists y:y\in\operatorname{dom}(R)\\ &\leftrightarrow\exists y:\exists z:x=(y,z)\wedge z\in\operatorname{cod}(R)\wedge y\in\operatorname{dom}(R)\\&\leftrightarrow\exists y\in\operatorname{dom}(R):\exists z\in\operatorname{cod}(R):x=(y,z)\\&\leftrightarrow x \in \operatorname{dom}(R)\times \operatorname{cod}(R) \end{align}$$

UPDATE (@Reese): $$\begin{align}x\in R \to\exists y:\exists z:x=(y,z)&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge (y,z)\in R \wedge (y,z)\in R\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge\exists z:(y,z)\in R\wedge\exists z:(y,z)\in R\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge\exists y:\exists z:(y,z)\in R\wedge\exists y:\exists z:(y,z)\in R\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge\exists y:y\in\operatorname{dom}(R)\wedge\exists z:\exists y:(y,z)\in R\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge\exists y:y\in\operatorname{dom}(R)\wedge \exists z:z\in \operatorname{cod}(R)\\&\leftrightarrow\exists y:\exists z:x=(y,z)\wedge z\in\operatorname{cod}(R)\wedge\exists y:y\in\operatorname{dom}(R)\\ &\leftrightarrow\exists y:\exists z:x=(y,z)\wedge z\in\operatorname{cod}(R)\wedge y\in\operatorname{dom}(R)\\&\leftrightarrow\exists y\in\operatorname{dom}(R):\exists z\in\operatorname{cod}(R):x=(y,z)\\&\leftrightarrow x \in \operatorname{dom}(R)\times \operatorname{cod}(R) \end{align}$$ Is it correct?

Answer 1

Let $R$ be a relation.

Let $(x_0,y_0)\in R$. Then $x_0\in \operatorname{dom}(R)$ and $y_0\in \operatorname{cod}(R)$, so $(x_0,y_0)\in \operatorname{dom}(R)\times \operatorname{cod}(R)$. Thus $R\subseteq\operatorname{dom}(R)\times \operatorname{cod}(R)$.

---

You can tell that what you've currently written is wrong because as Reese and Josh pointed out, the statement is $R\subseteq\operatorname{dom}(R)\times\operatorname{cod}(R)$, not equality. Your proof proves equality and therefore cannot be right. Your proof is also much more complicated than it needs to be. This works.

\begin{align}a\in R & \to\exists b:\exists c:a=(b,c)\\ &\to (b,c)\in R\\ &\to\exists y:(b,y)\in R\\ &\to b\in\operatorname{dom}(R)\\ &\to\exists y:(y,c)\in R\\ &\to c\in\operatorname{cod}(R)\\ &\to (b,c)\in\operatorname{dom}(R)\times\operatorname{cod}(R)\\ &\to a\in\operatorname{dom}(R)\times\operatorname{cod}(R) \end{align}