Theorem refrelsredund2

Description: The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 ) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022)

	Ref	Expression
Assertion	refrelsredund2	$$⊢\left\{r\in \mathrm{Rels}|{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\right\}Redund⟨\mathrm{RefRels},\mathrm{EqvRels}⟩$$

Proof

Step	Hyp	Ref	Expression
1		refrelsredund4	$$⊢\left\{r\in \mathrm{Rels}|{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\right\}Redund⟨\mathrm{RefRels},\left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)⟩$$
2		df-eqvrels	$$⊢\mathrm{EqvRels}=\left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)\cap \mathrm{TrRels}$$
3		inss1	$$⊢\left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)\cap \mathrm{TrRels}\subseteq \mathrm{RefRels}\cap \mathrm{SymRels}$$
4	2 3	eqsstri	$$⊢\mathrm{EqvRels}\subseteq \mathrm{RefRels}\cap \mathrm{SymRels}$$
5	4	redundss3	$$⊢\left\{r\in \mathrm{Rels}|{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\right\}Redund⟨\mathrm{RefRels},\left(\mathrm{RefRels}\cap \mathrm{SymRels}\right)⟩\to \left\{r\in \mathrm{Rels}|{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\right\}Redund⟨\mathrm{RefRels},\mathrm{EqvRels}⟩$$
6	1 5	ax-mp	$$⊢\left\{r\in \mathrm{Rels}|{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\right\}Redund⟨\mathrm{RefRels},\mathrm{EqvRels}⟩$$