Theorem refrelcoss

Description: The class of cosets by R is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020)

	Ref	Expression
Assertion	refrelcoss	$$⊢RefRel\wr R$$

Proof

Step	Hyp	Ref	Expression
1		refrelcoss2	$$⊢\left(\mathrm{I}\cap \left(\mathrm{dom}\wr R\times \mathrm{ran}\wr R\right)\subseteq \wr R\wedge \mathrm{Rel}\wr R\right)$$
2		dfrefrel2	$$⊢RefRel\wr R\leftrightarrow \left(\mathrm{I}\cap \left(\mathrm{dom}\wr R\times \mathrm{ran}\wr R\right)\subseteq \wr R\wedge \mathrm{Rel}\wr R\right)$$
3	1 2	mpbir	$$⊢RefRel\wr R$$