Metamath Proof Explorer


Theorem refrelcoss3

Description: The class of cosets by R is reflexive, see dfrefrel3 . (Contributed by Peter Mazsa, 30-Jul-2019)

Ref Expression
Assertion refrelcoss3 xdomRyranRx=yxRyRelR

Proof

Step Hyp Ref Expression
1 refrelcosslem xdomRxRx
2 idinxpssinxp4 xdomRydomRx=yxRyxdomRxRx
3 1 2 mpbir xdomRydomRx=yxRy
4 rncossdmcoss ranR=domR
5 4 raleqi yranRx=yxRyydomRx=yxRy
6 5 ralbii xdomRyranRx=yxRyxdomRydomRx=yxRy
7 3 6 mpbir xdomRyranRx=yxRy
8 relcoss RelR
9 7 8 pm3.2i xdomRyranRx=yxRyRelR