Metamath Proof Explorer


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 I

Proof

Step Hyp Ref Expression
1 relcoss Rel R
2 dfcnvrefrel2 CnvRefRel R R I dom R × ran R Rel R
3 1 2 mpbiran2 CnvRefRel R R I dom R × ran R
4 cossssid R I R I dom R × ran R
5 3 4 bitr4i CnvRefRel R R I