eleqvrels2

Description: Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021)

		Ref	Expression
	Assertion	eleqvrels2	$⊢ R \in EqvRels \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land R \in Rels)$

Step	Hyp	Ref	Expression
1		dfeqvrels2	$⊢ EqvRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r \land r \circ r \subseteq r)\}$
2		dmeq	$⊢ r = R \to dom r = dom R$
3	2	reseq2d	$⊢ r = R \to {I ↾}_{dom r} = {I ↾}_{dom R}$
4		id	$⊢ r = R \to r = R$
5	3 4	sseq12d	$⊢ r = R \to ({I ↾}_{dom r} \subseteq r \leftrightarrow {I ↾}_{dom R} \subseteq R)$
6		cnveq	$⊢ r = R \to r^{-1} = R^{-1}$
7	6 4	sseq12d	$⊢ r = R \to (r^{-1} \subseteq r \leftrightarrow R^{-1} \subseteq R)$
8		coideq	$⊢ r = R \to r \circ r = R \circ R$
9	8 4	sseq12d	$⊢ r = R \to (r \circ r \subseteq r \leftrightarrow R \circ R \subseteq R)$
10	5 7 9	3anbi123d	$⊢ r = R \to (({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r \land r \circ r \subseteq r) \leftrightarrow ({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R))$
11	1 10	rabeqel	$⊢ R \in EqvRels \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land R \in Rels)$

Metamath Proof Explorer