Theorem dfcoss3

Description: Alternate definition of the class of cosets by R (see the comment of df-coss ). (Contributed by Peter Mazsa, 27-Dec-2018)

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

Proof

Step	Hyp	Ref	Expression
1		brcnvg	$$⊢\left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\to \left(x{R}^{-1}u\leftrightarrow uRx\right)$$
2	1	el2v	$$⊢x{R}^{-1}u\leftrightarrow uRx$$
3	2	anbi1i	$$⊢\left(x{R}^{-1}u\wedge uRy\right)\leftrightarrow \left(uRx\wedge uRy\right)$$
4	3	exbii	$$⊢\exists u\left(x{R}^{-1}u\wedge uRy\right)\leftrightarrow \exists u\left(uRx\wedge uRy\right)$$
5	4	opabbii	$$⊢\left\{⟨x,y⟩|\exists u\left(x{R}^{-1}u\wedge uRy\right)\right\}=\left\{⟨x,y⟩|\exists u\left(uRx\wedge uRy\right)\right\}$$
6		df-co	$$⊢R\circ R^{-1}=\left\{⟨x,y⟩|\exists u\left(x{R}^{-1}u\wedge uRy\right)\right\}$$
7		df-coss	$$⊢\wr R=\left\{⟨x,y⟩|\exists u\left(uRx\wedge uRy\right)\right\}$$
8	5 6 7	3eqtr4ri	$$⊢\wr R=R\circ R^{-1}$$