Theorem disjxrn

Description: Two ways of saying that a range Cartesian product is disjoint. (Contributed by Peter Mazsa, 17-Jun-2020) (Revised by Peter Mazsa, 21-Sep-2021)

	Ref	Expression
Assertion	disjxrn	$$⊢DisjR⋉S\leftrightarrow \wr R^{-1}\cap \wr S^{-1}\subseteq \mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		xrnrel	$$⊢\mathrm{Rel}R⋉S$$
2		dfdisjALTV2	$$⊢DisjR⋉S\leftrightarrow \left(\wr {R⋉S}^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}R⋉S\right)$$
3	1 2	mpbiran2	$$⊢DisjR⋉S\leftrightarrow \wr {R⋉S}^{-1}\subseteq \mathrm{I}$$
4		1cosscnvxrn	$$⊢\wr {R⋉S}^{-1}=\wr R^{-1}\cap \wr S^{-1}$$
5	4	sseq1i	$$⊢\wr {R⋉S}^{-1}\subseteq \mathrm{I}\leftrightarrow \wr R^{-1}\cap \wr S^{-1}\subseteq \mathrm{I}$$
6	3 5	bitri	$$⊢DisjR⋉S\leftrightarrow \wr R^{-1}\cap \wr S^{-1}\subseteq \mathrm{I}$$