Theorem refrelsredund3

Description: The naive version of the class of reflexive relations { r e. Rels | A. x e. dom r x r x } is redundant with respect to the class of reflexive relations (see dfrefrels3 ) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022)

	Ref	Expression
Assertion	refrelsredund3	$$⊢\left\{r\in \mathrm{Rels}|\forall x\in \mathrm{dom}rxrx\right\}Redund⟨\mathrm{RefRels},\mathrm{EqvRels}⟩$$

Proof

Step	Hyp	Ref	Expression
1		refrelsredund2	$$⊢\left\{r\in \mathrm{Rels}|{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\right\}Redund⟨\mathrm{RefRels},\mathrm{EqvRels}⟩$$
2		idrefALT	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\leftrightarrow \forall x\in \mathrm{dom}rxrx$$
3	2	rabbii	$$⊢\left\{r\in \mathrm{Rels}|{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\right\}=\left\{r\in \mathrm{Rels}|\forall x\in \mathrm{dom}rxrx\right\}$$
4	3	redundeq1	$$⊢\left\{r\in \mathrm{Rels}|{\mathrm{I}\upharpoonright }_{\mathrm{dom}r}\subseteq r\right\}Redund⟨\mathrm{RefRels},\mathrm{EqvRels}⟩\leftrightarrow \left\{r\in \mathrm{Rels}|\forall x\in \mathrm{dom}rxrx\right\}Redund⟨\mathrm{RefRels},\mathrm{EqvRels}⟩$$
5	1 4	mpbi	$$⊢\left\{r\in \mathrm{Rels}|\forall x\in \mathrm{dom}rxrx\right\}Redund⟨\mathrm{RefRels},\mathrm{EqvRels}⟩$$