Theorem refrelredund2

Description: The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 ) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022)

	Ref	Expression
Assertion	refrelredund2	|- redund ( ( ( _I |` dom R ) C_ R /\ Rel R ) , RefRel R , EqvRel R )

Proof

Step	Hyp	Ref	Expression
1		refrelredund4	|- redund ( ( ( _I |` dom R ) C_ R /\ Rel R ) , RefRel R , ( RefRel R /\ SymRel R ) )
2		df-eqvrel	|- ( EqvRel R <-> ( RefRel R /\ SymRel R /\ TrRel R ) )
3		3simpa	|- ( ( RefRel R /\ SymRel R /\ TrRel R ) -> ( RefRel R /\ SymRel R ) )
4	2 3	sylbi	|- ( EqvRel R -> ( RefRel R /\ SymRel R ) )
5	4	redundpim3	|- ( redund ( ( ( _I |` dom R ) C_ R /\ Rel R ) , RefRel R , ( RefRel R /\ SymRel R ) ) -> redund ( ( ( _I |` dom R ) C_ R /\ Rel R ) , RefRel R , EqvRel R ) )
6	1 5	ax-mp	|- redund ( ( ( _I |` dom R ) C_ R /\ Rel R ) , RefRel R , EqvRel R )