# Metamath Proof Explorer

## Theorem xptrrel

Description: The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion xptrrel ${⊢}\left({A}×{B}\right)\circ \left({A}×{B}\right)\subseteq {A}×{B}$

### Proof

Step Hyp Ref Expression
1 inss1 ${⊢}\mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)\subseteq \mathrm{dom}\left({A}×{B}\right)$
2 dmxpss ${⊢}\mathrm{dom}\left({A}×{B}\right)\subseteq {A}$
3 1 2 sstri ${⊢}\mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)\subseteq {A}$
4 inss2 ${⊢}\mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)\subseteq \mathrm{ran}\left({A}×{B}\right)$
5 rnxpss ${⊢}\mathrm{ran}\left({A}×{B}\right)\subseteq {B}$
6 4 5 sstri ${⊢}\mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)\subseteq {B}$
7 3 6 ssini ${⊢}\mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)\subseteq {A}\cap {B}$
8 eqimss ${⊢}{A}\cap {B}=\varnothing \to {A}\cap {B}\subseteq \varnothing$
9 7 8 sstrid ${⊢}{A}\cap {B}=\varnothing \to \mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)\subseteq \varnothing$
10 ss0 ${⊢}\mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)\subseteq \varnothing \to \mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)=\varnothing$
11 9 10 syl ${⊢}{A}\cap {B}=\varnothing \to \mathrm{dom}\left({A}×{B}\right)\cap \mathrm{ran}\left({A}×{B}\right)=\varnothing$
12 11 coemptyd ${⊢}{A}\cap {B}=\varnothing \to \left({A}×{B}\right)\circ \left({A}×{B}\right)=\varnothing$
13 0ss ${⊢}\varnothing \subseteq {A}×{B}$
14 12 13 eqsstrdi ${⊢}{A}\cap {B}=\varnothing \to \left({A}×{B}\right)\circ \left({A}×{B}\right)\subseteq {A}×{B}$
15 neqne ${⊢}¬{A}\cap {B}=\varnothing \to {A}\cap {B}\ne \varnothing$
16 15 xpcoidgend ${⊢}¬{A}\cap {B}=\varnothing \to \left({A}×{B}\right)\circ \left({A}×{B}\right)={A}×{B}$
17 ssid ${⊢}{A}×{B}\subseteq {A}×{B}$
18 16 17 eqsstrdi ${⊢}¬{A}\cap {B}=\varnothing \to \left({A}×{B}\right)\circ \left({A}×{B}\right)\subseteq {A}×{B}$
19 14 18 pm2.61i ${⊢}\left({A}×{B}\right)\circ \left({A}×{B}\right)\subseteq {A}×{B}$