Theorem cosscnvssid4

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

	Ref	Expression
Assertion	cosscnvssid4	$$⊢\wr R^{-1}\subseteq \mathrm{I}\leftrightarrow \forall x{\exists }^{*}uuRx$$

Proof

Step	Hyp	Ref	Expression
1		cossssid4	$$⊢\wr R^{-1}\subseteq \mathrm{I}\leftrightarrow \forall x{\exists }^{*}ux{R}^{-1}u$$
2		brcnvg	$$⊢\left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\to \left(x{R}^{-1}u\leftrightarrow uRx\right)$$
3	2	el2v	$$⊢x{R}^{-1}u\leftrightarrow uRx$$
4	3	mobii	$$⊢{\exists }^{*}ux{R}^{-1}u\leftrightarrow {\exists }^{*}uuRx$$
5	4	albii	$$⊢\forall x{\exists }^{*}ux{R}^{-1}u\leftrightarrow \forall x{\exists }^{*}uuRx$$
6	1 5	bitri	$$⊢\wr R^{-1}\subseteq \mathrm{I}\leftrightarrow \forall x{\exists }^{*}uuRx$$