Metamath Proof Explorer

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}×\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}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}$
3 19.8a ${⊢}⟨{x},{y}⟩\in {A}\to \exists {x}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}$
4 opelxp ${⊢}⟨{x},{y}⟩\in \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)↔\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}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}$
7 vex ${⊢}{y}\in \mathrm{V}$
8 7 elrn2 ${⊢}{y}\in \mathrm{ran}{A}↔\exists {x}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}$
9 6 8 anbi12i ${⊢}\left({x}\in \mathrm{dom}{A}\wedge {y}\in \mathrm{ran}{A}\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}\wedge \exists {x}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}\right)$
10 4 9 bitri ${⊢}⟨{x},{y}⟩\in \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}\wedge \exists {x}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}\right)$
11 2 3 10 sylanbrc ${⊢}⟨{x},{y}⟩\in {A}\to ⟨{x},{y}⟩\in \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)$
12 11 a1i ${⊢}\mathrm{Rel}{A}\to \left(⟨{x},{y}⟩\in {A}\to ⟨{x},{y}⟩\in \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)$
13 1 12 relssdv ${⊢}\mathrm{Rel}{A}\to {A}\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$