Theorem eqvrelcoss2

Description: Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019)

	Ref	Expression
Assertion	eqvrelcoss2	$$⊢EqvRel\wr R\leftrightarrow \wr \wr R\subseteq \wr R$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelcoss3	$$⊢EqvRel\wr R\leftrightarrow \forall x\forall y\forall z\left(\left(x\wr Ry\wedge y\wr Rz\right)\to x\wr Rz\right)$$
2		cocossss	$$⊢\wr \wr R\subseteq \wr R\leftrightarrow \forall x\forall y\forall z\left(\left(x\wr Ry\wedge y\wr Rz\right)\to x\wr Rz\right)$$
3	1 2	bitr4i	$$⊢EqvRel\wr R\leftrightarrow \wr \wr R\subseteq \wr R$$