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} \subseteq R \land Rel R), RefRel R, (RefRel R \land SymRel R))$

Proof

Step	Hyp	Ref	Expression
1		inxpssres	$⊢ I \cap (dom R \times ran R) \subseteq {I ↾}_{dom R}$
2		sstr2	$⊢ I \cap (dom R \times ran R) \subseteq {I ↾}_{dom R} \to ({I ↾}_{dom R} \subseteq R \to I \cap (dom R \times ran R) \subseteq R)$
3	1 2	ax-mp	$⊢ {I ↾}_{dom R} \subseteq R \to I \cap (dom R \times ran R) \subseteq R$
4	3	anim1i	$⊢ ({I ↾}_{dom R} \subseteq R \land Rel R) \to (I \cap (dom R \times ran R) \subseteq R \land Rel R)$
5		dfrefrel2	$⊢ RefRel R \leftrightarrow (I \cap (dom R \times ran R) \subseteq R \land Rel R)$
6	4 5	sylibr	$⊢ ({I ↾}_{dom R} \subseteq R \land Rel R) \to RefRel R$
7		an12	$⊢ (({I ↾}_{dom R} \subseteq R \land Rel R) \land (RefRel R \land SymRel R)) \leftrightarrow (RefRel R \land (({I ↾}_{dom R} \subseteq R \land Rel R) \land SymRel R))$
8		anandir	$⊢ (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land Rel R) \land (R^{-1} \subseteq R \land Rel R))$
9		refsymrel2	$⊢ (RefRel R \land SymRel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R)$
10		dfsymrel2	$⊢ SymRel R \leftrightarrow (R^{-1} \subseteq R \land Rel R)$
11	10	anbi2i	$⊢ (({I ↾}_{dom R} \subseteq R \land Rel R) \land SymRel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land Rel R) \land (R^{-1} \subseteq R \land Rel R))$
12	8 9 11	3bitr4i	$⊢ (RefRel R \land SymRel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land Rel R) \land SymRel R)$
13	12	anbi2i	$⊢ (RefRel R \land (RefRel R \land SymRel R)) \leftrightarrow (RefRel R \land (({I ↾}_{dom R} \subseteq R \land Rel R) \land SymRel R))$
14	7 13	bitr4i	$⊢ (({I ↾}_{dom R} \subseteq R \land Rel R) \land (RefRel R \land SymRel R)) \leftrightarrow (RefRel R \land (RefRel R \land SymRel R))$
15		df-redundp	$⊢ redund (({I ↾}_{dom R} \subseteq R \land Rel R), RefRel R, (RefRel R \land SymRel R)) \leftrightarrow ((({I ↾}_{dom R} \subseteq R \land Rel R) \to RefRel R) \land ((({I ↾}_{dom R} \subseteq R \land Rel R) \land (RefRel R \land SymRel R)) \leftrightarrow (RefRel R \land (RefRel R \land SymRel R))))$
16	6 14 15	mpbir2an	$⊢ redund (({I ↾}_{dom R} \subseteq R \land Rel R), RefRel R, (RefRel R \land SymRel R))$