dfeqvrels2

Description: Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019)

		Ref	Expression
	Assertion	dfeqvrels2	$⊢ EqvRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r \land r \circ r \subseteq r)\}$

Step	Hyp	Ref	Expression
1		df-eqvrels	$⊢ EqvRels = (RefRels \cap SymRels) \cap TrRels$
2		refsymrels2	$⊢ RefRels \cap SymRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\}$
3		dftrrels2	$⊢ TrRels = \{r \in Rels \| r \circ r \subseteq r\}$
4	2 3	ineq12i	$⊢ (RefRels \cap SymRels) \cap TrRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\} \cap \{r \in Rels \| r \circ r \subseteq r\}$
5		inrab	$⊢ \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\} \cap \{r \in Rels \| r \circ r \subseteq r\} = \{r \in Rels \| (({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r) \land r \circ r \subseteq r)\}$
6	1 4 5	3eqtri	$⊢ EqvRels = \{r \in Rels \| (({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r) \land r \circ r \subseteq r)\}$
7		df-3an	$⊢ ({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)$
8	7	rabbii	$⊢ \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r \land r \circ r \subseteq r)\} = \{r \in Rels \| (({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r) \land r \circ r \subseteq r)\}$
9	6 8	eqtr4i	$⊢ EqvRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r \land r \circ r \subseteq r)\}$

Metamath Proof Explorer