Metamath Proof Explorer

Theorem refrelredund4

Description: The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 ) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022)

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

Proof

Step	Hyp	Ref	Expression
1		inxpssres	\|- ( _I i^i ( dom R X. ran R ) ) C_ ( _I \|` dom R )
2		sstr2	\|- ( ( _I i^i ( dom R X. ran R ) ) C_ ( _I \|` dom R ) -> ( ( _I \|` dom R ) C_ R -> ( _I i^i ( dom R X. ran R ) ) C_ R ) )
3	1 2	ax-mp	\|- ( ( _I \|` dom R ) C_ R -> ( _I i^i ( dom R X. ran R ) ) C_ R )
4	3	anim1i	\|- ( ( ( _I \|` dom R ) C_ R /\ Rel R ) -> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )
5		dfrefrel2	\|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )
6	4 5	sylibr	\|- ( ( ( _I \|` dom R ) C_ R /\ Rel R ) -> RefRel R )
7		an12	\|- ( ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ ( RefRel R /\ SymRel R ) ) <-> ( RefRel R /\ ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ SymRel R ) ) )
8		anandir	\|- ( ( ( ( _I \|` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) <-> ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ ( `' R C_ R /\ Rel R ) ) )
9		refsymrel2	\|- ( ( RefRel R /\ SymRel R ) <-> ( ( ( _I \|` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) )
10		dfsymrel2	\|- ( SymRel R <-> ( `' R C_ R /\ Rel R ) )
11	10	anbi2i	\|- ( ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ SymRel R ) <-> ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ ( `' R C_ R /\ Rel R ) ) )
12	8 9 11	3bitr4i	\|- ( ( RefRel R /\ SymRel R ) <-> ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ SymRel R ) )
13	12	anbi2i	\|- ( ( RefRel R /\ ( RefRel R /\ SymRel R ) ) <-> ( RefRel R /\ ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ SymRel R ) ) )
14	7 13	bitr4i	\|- ( ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ ( RefRel R /\ SymRel R ) ) <-> ( RefRel R /\ ( RefRel R /\ SymRel R ) ) )
15		df-redundp	\|- ( redund ( ( ( _I \|` dom R ) C_ R /\ Rel R ) , RefRel R , ( RefRel R /\ SymRel R ) ) <-> ( ( ( ( _I \|` dom R ) C_ R /\ Rel R ) -> RefRel R ) /\ ( ( ( ( _I \|` dom R ) C_ R /\ Rel R ) /\ ( RefRel R /\ SymRel R ) ) <-> ( RefRel R /\ ( RefRel R /\ SymRel R ) ) ) ) )
16	6 14 15	mpbir2an	\|- redund ( ( ( _I \|` dom R ) C_ R /\ Rel R ) , RefRel R , ( RefRel R /\ SymRel R ) )