Theorem eqvrelcoss4

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

	Ref	Expression
Assertion	eqvrelcoss4	$$⊢EqvRel\wr R\leftrightarrow \forall x\forall z\left(\left[x\right]\wr R\cap \left[z\right]\wr R\ne \varnothing \to \left[x\right]R^{-1}\cap \left[z\right]R^{-1}\ne \varnothing \right)$$

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		trcoss2	$$⊢\forall x\forall y\forall z\left(\left(x\wr Ry\wedge y\wr Rz\right)\to x\wr Rz\right)\leftrightarrow \forall x\forall z\left(\left[x\right]\wr R\cap \left[z\right]\wr R\ne \varnothing \to \left[x\right]R^{-1}\cap \left[z\right]R^{-1}\ne \varnothing \right)$$
3	1 2	bitri	$$⊢EqvRel\wr R\leftrightarrow \forall x\forall z\left(\left[x\right]\wr R\cap \left[z\right]\wr R\ne \varnothing \to \left[x\right]R^{-1}\cap \left[z\right]R^{-1}\ne \varnothing \right)$$