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	|- { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , EqvRels >.

Proof

Step	Hyp	Ref	Expression
1		refrelsredund4	|- { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , ( RefRels i^i SymRels ) >.
2		df-eqvrels	|- EqvRels = ( ( RefRels i^i SymRels ) i^i TrRels )
3		inss1	|- ( ( RefRels i^i SymRels ) i^i TrRels ) C_ ( RefRels i^i SymRels )
4	2 3	eqsstri	|- EqvRels C_ ( RefRels i^i SymRels )
5	4	redundss3	|- ( { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , ( RefRels i^i SymRels ) >. -> { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , EqvRels >. )
6	1 5	ax-mp	|- { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , EqvRels >.