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 ,~ R <-> ,~ R C_ _I )

Proof

Step	Hyp	Ref	Expression
1		relcoss	|- Rel ,~ R
2		dfcnvrefrel2	|- ( CnvRefRel ,~ R <-> ( ,~ R C_ ( _I i^i ( dom ,~ R X. ran ,~ R ) ) /\ Rel ,~ R ) )
3	1 2	mpbiran2	|- ( CnvRefRel ,~ R <-> ,~ R C_ ( _I i^i ( dom ,~ R X. ran ,~ R ) ) )
4		cossssid	|- ( ,~ R C_ _I <-> ,~ R C_ ( _I i^i ( dom ,~ R X. ran ,~ R ) ) )
5	3 4	bitr4i	|- ( CnvRefRel ,~ R <-> ,~ R C_ _I )