Theorem refrelcoss3

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

	Ref	Expression
Assertion	refrelcoss3	|- ( A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) /\ Rel ,~ R )

Proof

Step	Hyp	Ref	Expression
1		refrelcosslem	|- A. x e. dom ,~ R x ,~ R x
2		idinxpssinxp4	|- ( A. x e. dom ,~ R A. y e. dom ,~ R ( x = y -> x ,~ R y ) <-> A. x e. dom ,~ R x ,~ R x )
3	1 2	mpbir	|- A. x e. dom ,~ R A. y e. dom ,~ R ( x = y -> x ,~ R y )
4		rncossdmcoss	|- ran ,~ R = dom ,~ R
5	4	raleqi	|- ( A. y e. ran ,~ R ( x = y -> x ,~ R y ) <-> A. y e. dom ,~ R ( x = y -> x ,~ R y ) )
6	5	ralbii	|- ( A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) <-> A. x e. dom ,~ R A. y e. dom ,~ R ( x = y -> x ,~ R y ) )
7	3 6	mpbir	|- A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y )
8		relcoss	|- Rel ,~ R
9	7 8	pm3.2i	|- ( A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) /\ Rel ,~ R )