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) (Proof shortened by SN, 23-Dec-2024)

	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		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	opeldm	$$⊢⟨x,y⟩\in A\to x\in \mathrm{dom}A$$
5	2 3	opelrn	$$⊢⟨x,y⟩\in A\to y\in \mathrm{ran}A$$
6	4 5	opelxpd	$$⊢⟨x,y⟩\in A\to ⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)$$
7	6	a1i	$$⊢\mathrm{Rel}A\to \left(⟨x,y⟩\in A\to ⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)$$
8	1 7	relssdv	$$⊢\mathrm{Rel}A\to A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$