Theorem relssdmrn

Description: A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of Mendelson p. 235. (Contributed by NM, 3-Aug-1994)

	Ref	Expression
Assertion	relssdmrn	$$⊢\mathrm{Rel}A\to A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\mathrm{Rel}A\to \mathrm{Rel}A$$
2		19.8a	$$⊢⟨x,y⟩\in A\to \exists y⟨x,y⟩\in A$$
3		19.8a	$$⊢⟨x,y⟩\in A\to \exists x⟨x,y⟩\in A$$
4		opelxp	$$⊢⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)\leftrightarrow \left(x\in \mathrm{dom}A\wedge y\in \mathrm{ran}A\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	eldm2	$$⊢x\in \mathrm{dom}A\leftrightarrow \exists y⟨x,y⟩\in A$$
7		vex	$$⊢y\in \mathrm{V}$$
8	7	elrn2	$$⊢y\in \mathrm{ran}A\leftrightarrow \exists x⟨x,y⟩\in A$$
9	6 8	anbi12i	$$⊢\left(x\in \mathrm{dom}A\wedge y\in \mathrm{ran}A\right)\leftrightarrow \left(\exists y⟨x,y⟩\in A\wedge \exists x⟨x,y⟩\in A\right)$$
10	4 9	bitri	$$⊢⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)\leftrightarrow \left(\exists y⟨x,y⟩\in A\wedge \exists x⟨x,y⟩\in A\right)$$
11	2 3 10	sylanbrc	$$⊢⟨x,y⟩\in A\to ⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)$$
12	11	a1i	$$⊢\mathrm{Rel}A\to \left(⟨x,y⟩\in A\to ⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)$$
13	1 12	relssdv	$$⊢\mathrm{Rel}A\to A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$