Theorem disjorimxrn

Description: Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 12-Jul-2020) (Revised by Peter Mazsa, 22-Sep-2021)

	Ref	Expression
Assertion	disjorimxrn	$$⊢\left(DisjR\vee DisjS\right)\to DisjR⋉S$$

Proof

Step	Hyp	Ref	Expression
1		dfdisjALTV2	$$⊢DisjR\leftrightarrow \left(\wr R^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}R\right)$$
2	1	simplbi	$$⊢DisjR\to \wr R^{-1}\subseteq \mathrm{I}$$
3		dfdisjALTV2	$$⊢DisjS\leftrightarrow \left(\wr S^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}S\right)$$
4	3	simplbi	$$⊢DisjS\to \wr S^{-1}\subseteq \mathrm{I}$$
5	2 4	orim12i	$$⊢\left(DisjR\vee DisjS\right)\to \left(\wr R^{-1}\subseteq \mathrm{I}\vee \wr S^{-1}\subseteq \mathrm{I}\right)$$
6		inss	$$⊢\left(\wr R^{-1}\subseteq \mathrm{I}\vee \wr S^{-1}\subseteq \mathrm{I}\right)\to \wr R^{-1}\cap \wr S^{-1}\subseteq \mathrm{I}$$
7	5 6	syl	$$⊢\left(DisjR\vee DisjS\right)\to \wr R^{-1}\cap \wr S^{-1}\subseteq \mathrm{I}$$
8		disjxrn	$$⊢DisjR⋉S\leftrightarrow \wr R^{-1}\cap \wr S^{-1}\subseteq \mathrm{I}$$
9	7 8	sylibr	$$⊢\left(DisjR\vee DisjS\right)\to DisjR⋉S$$