Theorem cossssid4

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 31-Aug-2021)

	Ref	Expression
Assertion	cossssid4	$$⊢\wr R\subseteq \mathrm{I}\leftrightarrow \forall u{\exists }^{*}xuRx$$

Proof

Step	Hyp	Ref	Expression
1		cossssid3	$$⊢\wr R\subseteq \mathrm{I}\leftrightarrow \forall u\forall x\forall y\left(\left(uRx\wedge uRy\right)\to x=y\right)$$
2		breq2	$$⊢x=y\to \left(uRx\leftrightarrow uRy\right)$$
3	2	mo4	$$⊢{\exists }^{*}xuRx\leftrightarrow \forall x\forall y\left(\left(uRx\wedge uRy\right)\to x=y\right)$$
4	3	albii	$$⊢\forall u{\exists }^{*}xuRx\leftrightarrow \forall u\forall x\forall y\left(\left(uRx\wedge uRy\right)\to x=y\right)$$
5	1 4	bitr4i	$$⊢\wr R\subseteq \mathrm{I}\leftrightarrow \forall u{\exists }^{*}xuRx$$