Theorem symrelcoss3

Description: The class of cosets by R is symmetric, see dfsymrel3 . (Contributed by Peter Mazsa, 28-Mar-2019) (Revised by Peter Mazsa, 17-Sep-2021)

	Ref	Expression
Assertion	symrelcoss3	$$⊢\left(\forall x\forall y\left(x\wr Ry\to y\wr Rx\right)\wedge \mathrm{Rel}\wr R\right)$$

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		relcoss	$$⊢\mathrm{Rel}\wr R$$
6	4 5	pm3.2i	$$⊢\left(\forall x\forall y\left(x\wr Ry\to y\wr Rx\right)\wedge \mathrm{Rel}\wr R\right)$$