Theorem xptrrel

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

	Ref	Expression
Assertion	xptrrel	$$⊢\left(A\times B\right)\circ \left(A\times B\right)\subseteq A\times B$$

Proof

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