Theorem symrelcoss

Description: The class of cosets by R is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021)

	Ref	Expression
Assertion	symrelcoss	$$⊢SymRel\wr R$$

Proof

Step	Hyp	Ref	Expression
1		symrelcoss2	$$⊢\left({\wr R}^{-1}\subseteq \wr R\wedge \mathrm{Rel}\wr R\right)$$
2		dfsymrel2	$$⊢SymRel\wr R\leftrightarrow \left({\wr R}^{-1}\subseteq \wr R\wedge \mathrm{Rel}\wr R\right)$$
3	1 2	mpbir	$$⊢SymRel\wr R$$