Theorem br2coss

Description: Cosets by ,R binary relation. (Contributed by Peter Mazsa, 25-Aug-2019)

	Ref	Expression
Assertion	br2coss	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\wr \wr RB\leftrightarrow \left[A\right]\wr R\cap \left[B\right]\wr R\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		brcoss3	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\wr \wr RB\leftrightarrow \left[A\right]{\wr R}^{-1}\cap \left[B\right]{\wr R}^{-1}\ne \varnothing \right)$$
2		cnvcosseq	$$⊢{\wr R}^{-1}=\wr R$$
3	2	eceq2i	$$⊢\left[A\right]{\wr R}^{-1}=\left[A\right]\wr R$$
4	2	eceq2i	$$⊢\left[B\right]{\wr R}^{-1}=\left[B\right]\wr R$$
5	3 4	ineq12i	$$⊢\left[A\right]{\wr R}^{-1}\cap \left[B\right]{\wr R}^{-1}=\left[A\right]\wr R\cap \left[B\right]\wr R$$
6	5	neeq1i	$$⊢\left[A\right]{\wr R}^{-1}\cap \left[B\right]{\wr R}^{-1}\ne \varnothing \leftrightarrow \left[A\right]\wr R\cap \left[B\right]\wr R\ne \varnothing$$
7	1 6	bitrdi	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\wr \wr RB\leftrightarrow \left[A\right]\wr R\cap \left[B\right]\wr R\ne \varnothing \right)$$