Theorem cnvcosseq

Description: The converse of cosets by R are cosets by R . (Contributed by Peter Mazsa, 3-May-2019)

	Ref	Expression
Assertion	cnvcosseq	$$⊢{\wr R}^{-1}=\wr R$$

Proof

Step	Hyp	Ref	Expression
1		brcosscnvcoss	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\to \left(x\wr Ry\leftrightarrow y\wr Rx\right)$$
2	1	el2v	$$⊢x\wr Ry\leftrightarrow y\wr Rx$$
3	2	biimpi	$$⊢x\wr Ry\to y\wr Rx$$
4	3	gen2	$$⊢\forall x\forall y\left(x\wr Ry\to y\wr Rx\right)$$
5		cnvsym	$$⊢{\wr R}^{-1}\subseteq \wr R\leftrightarrow \forall x\forall y\left(x\wr Ry\to y\wr Rx\right)$$
6	4 5	mpbir	$$⊢{\wr R}^{-1}\subseteq \wr R$$
7		relcoss	$$⊢\mathrm{Rel}\wr R$$
8		relcnveq	$$⊢\mathrm{Rel}\wr R\to \left({\wr R}^{-1}\subseteq \wr R\leftrightarrow {\wr R}^{-1}=\wr R\right)$$
9	7 8	ax-mp	$$⊢{\wr R}^{-1}\subseteq \wr R\leftrightarrow {\wr R}^{-1}=\wr R$$
10	6 9	mpbi	$$⊢{\wr R}^{-1}=\wr R$$