refrelcoss3

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

		Ref	Expression
	Assertion	refrelcoss3	$⊢ (\forall x \in dom ≀ R \forall y \in ran ≀ R (x = y \to x ≀ R y) \land Rel ≀ R)$

Step	Hyp	Ref	Expression
1		refrelcosslem	$⊢ \forall x \in dom ≀ R x ≀ R x$
2		idinxpssinxp4	$⊢ \forall x \in dom ≀ R \forall y \in dom ≀ R (x = y \to x ≀ R y) \leftrightarrow \forall x \in dom ≀ R x ≀ R x$
3	1 2	mpbir	$⊢ \forall x \in dom ≀ R \forall y \in dom ≀ R (x = y \to x ≀ R y)$
4		rncossdmcoss	$⊢ ran ≀ R = dom ≀ R$
5	4	raleqi	$⊢ \forall y \in ran ≀ R (x = y \to x ≀ R y) \leftrightarrow \forall y \in dom ≀ R (x = y \to x ≀ R y)$
6	5	ralbii	$⊢ \forall x \in dom ≀ R \forall y \in ran ≀ R (x = y \to x ≀ R y) \leftrightarrow \forall x \in dom ≀ R \forall y \in dom ≀ R (x = y \to x ≀ R y)$
7	3 6	mpbir	$⊢ \forall x \in dom ≀ R \forall y \in ran ≀ R (x = y \to x ≀ R y)$
8		relcoss	$⊢ Rel ≀ R$
9	7 8	pm3.2i	$⊢ (\forall x \in dom ≀ R \forall y \in ran ≀ R (x = y \to x ≀ R y) \land Rel ≀ R)$

Metamath Proof Explorer