# Metamath Proof Explorer

## Theorem relrelss

Description: Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008)

Ref Expression
Assertion relrelss ${⊢}\left(\mathrm{Rel}{A}\wedge \mathrm{Rel}\mathrm{dom}{A}\right)↔{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}$

### Proof

Step Hyp Ref Expression
1 df-rel ${⊢}\mathrm{Rel}\mathrm{dom}{A}↔\mathrm{dom}{A}\subseteq \mathrm{V}×\mathrm{V}$
2 1 anbi2i ${⊢}\left(\mathrm{Rel}{A}\wedge \mathrm{Rel}\mathrm{dom}{A}\right)↔\left(\mathrm{Rel}{A}\wedge \mathrm{dom}{A}\subseteq \mathrm{V}×\mathrm{V}\right)$
3 relssdmrn ${⊢}\mathrm{Rel}{A}\to {A}\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
4 ssv ${⊢}\mathrm{ran}{A}\subseteq \mathrm{V}$
5 xpss12 ${⊢}\left(\mathrm{dom}{A}\subseteq \mathrm{V}×\mathrm{V}\wedge \mathrm{ran}{A}\subseteq \mathrm{V}\right)\to \mathrm{dom}{A}×\mathrm{ran}{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}$
6 4 5 mpan2 ${⊢}\mathrm{dom}{A}\subseteq \mathrm{V}×\mathrm{V}\to \mathrm{dom}{A}×\mathrm{ran}{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}$
7 3 6 sylan9ss ${⊢}\left(\mathrm{Rel}{A}\wedge \mathrm{dom}{A}\subseteq \mathrm{V}×\mathrm{V}\right)\to {A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}$
8 xpss ${⊢}\left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\subseteq \mathrm{V}×\mathrm{V}$
9 sstr ${⊢}\left({A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\wedge \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\subseteq \mathrm{V}×\mathrm{V}\right)\to {A}\subseteq \mathrm{V}×\mathrm{V}$
10 8 9 mpan2 ${⊢}{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\to {A}\subseteq \mathrm{V}×\mathrm{V}$
11 df-rel ${⊢}\mathrm{Rel}{A}↔{A}\subseteq \mathrm{V}×\mathrm{V}$
12 10 11 sylibr ${⊢}{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\to \mathrm{Rel}{A}$
13 dmss ${⊢}{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\to \mathrm{dom}{A}\subseteq \mathrm{dom}\left(\left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\right)$
14 vn0 ${⊢}\mathrm{V}\ne \varnothing$
15 dmxp ${⊢}\mathrm{V}\ne \varnothing \to \mathrm{dom}\left(\left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\right)=\mathrm{V}×\mathrm{V}$
16 14 15 ax-mp ${⊢}\mathrm{dom}\left(\left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\right)=\mathrm{V}×\mathrm{V}$
17 13 16 sseqtrdi ${⊢}{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\to \mathrm{dom}{A}\subseteq \mathrm{V}×\mathrm{V}$
18 12 17 jca ${⊢}{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\to \left(\mathrm{Rel}{A}\wedge \mathrm{dom}{A}\subseteq \mathrm{V}×\mathrm{V}\right)$
19 7 18 impbii ${⊢}\left(\mathrm{Rel}{A}\wedge \mathrm{dom}{A}\subseteq \mathrm{V}×\mathrm{V}\right)↔{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}$
20 2 19 bitri ${⊢}\left(\mathrm{Rel}{A}\wedge \mathrm{Rel}\mathrm{dom}{A}\right)↔{A}\subseteq \left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}$