Theorem cnvrefrelcoss2

Description: Necessary and sufficient condition for a coset relation to be a converse reflexive relation. (Contributed by Peter Mazsa, 27-Jul-2021)

	Ref	Expression
Assertion	cnvrefrelcoss2	$$⊢CnvRefRel\wr R\leftrightarrow \wr R\subseteq \mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		relcoss	$$⊢\mathrm{Rel}\wr R$$
2		dfcnvrefrel2	$$⊢CnvRefRel\wr R\leftrightarrow \left(\wr R\subseteq \mathrm{I}\cap \left(\mathrm{dom}\wr R\times \mathrm{ran}\wr R\right)\wedge \mathrm{Rel}\wr R\right)$$
3	1 2	mpbiran2	$$⊢CnvRefRel\wr R\leftrightarrow \wr R\subseteq \mathrm{I}\cap \left(\mathrm{dom}\wr R\times \mathrm{ran}\wr R\right)$$
4		cossssid	$$⊢\wr R\subseteq \mathrm{I}\leftrightarrow \wr R\subseteq \mathrm{I}\cap \left(\mathrm{dom}\wr R\times \mathrm{ran}\wr R\right)$$
5	3 4	bitr4i	$$⊢CnvRefRel\wr R\leftrightarrow \wr R\subseteq \mathrm{I}$$