refsymrel2

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the restricted version for their reflexive part (see below), not just the (I i^i ( dom R X. ran R ) ) C R version of dfrefrel2 , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 23-Aug-2021)

		Ref	Expression
	Assertion	refsymrel2	$⊢ (RefRel R \land SymRel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R)$

Proof

Step	Hyp	Ref	Expression
1		dfrefrel2	$⊢ RefRel R \leftrightarrow (I \cap (dom R \times ran R) \subseteq R \land Rel R)$
2		dfsymrel2	$⊢ SymRel R \leftrightarrow (R^{-1} \subseteq R \land Rel R)$
3	1 2	anbi12i	$⊢ (RefRel R \land SymRel R) \leftrightarrow ((I \cap (dom R \times ran R) \subseteq R \land Rel R) \land (R^{-1} \subseteq R \land Rel R))$
4		anandi3r	$⊢ (I \cap (dom R \times ran R) \subseteq R \land Rel R \land R^{-1} \subseteq R) \leftrightarrow ((I \cap (dom R \times ran R) \subseteq R \land Rel R) \land (R^{-1} \subseteq R \land Rel R))$
5		3anan32	$⊢ (I \cap (dom R \times ran R) \subseteq R \land Rel R \land R^{-1} \subseteq R) \leftrightarrow ((I \cap (dom R \times ran R) \subseteq R \land R^{-1} \subseteq R) \land Rel R)$
6	3 4 5	3bitr2i	$⊢ (RefRel R \land SymRel R) \leftrightarrow ((I \cap (dom R \times ran R) \subseteq R \land R^{-1} \subseteq R) \land Rel R)$
7		symrefref2	$⊢ R^{-1} \subseteq R \to (I \cap (dom R \times ran R) \subseteq R \leftrightarrow {I ↾}_{dom R} \subseteq R)$
8	7	pm5.32ri	$⊢ (I \cap (dom R \times ran R) \subseteq R \land R^{-1} \subseteq R) \leftrightarrow ({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R)$
9	8	anbi1i	$⊢ ((I \cap (dom R \times ran R) \subseteq R \land R^{-1} \subseteq R) \land Rel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R)$
10	6 9	bitri	$⊢ (RefRel R \land SymRel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R)$

Metamath Proof Explorer

Theorem refsymrel2

Proof