eltrrels3

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

		Ref	Expression
	Assertion	eltrrels3	$⊢ R \in TrRels \leftrightarrow (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land R \in Rels)$

Step	Hyp	Ref	Expression
1		dftrrels3	$⊢ TrRels = \{r \in Rels \| \forall x \forall y \forall z ((x r y \land y r z) \to x r z)\}$
2		breq	$⊢ r = R \to (x r y \leftrightarrow x R y)$
3		breq	$⊢ r = R \to (y r z \leftrightarrow y R z)$
4	2 3	anbi12d	$⊢ r = R \to ((x r y \land y r z) \leftrightarrow (x R y \land y R z))$
5		breq	$⊢ r = R \to (x r z \leftrightarrow x R z)$
6	4 5	imbi12d	$⊢ r = R \to (((x r y \land y r z) \to x r z) \leftrightarrow ((x R y \land y R z) \to x R z))$
7	6	2albidv	$⊢ r = R \to (\forall y \forall z ((x r y \land y r z) \to x r z) \leftrightarrow \forall y \forall z ((x R y \land y R z) \to x R z))$
8	7	albidv	$⊢ r = R \to (\forall x \forall y \forall z ((x r y \land y r z) \to x r z) \leftrightarrow \forall x \forall y \forall z ((x R y \land y R z) \to x R z))$
9	1 8	rabeqel	$⊢ R \in TrRels \leftrightarrow (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land R \in Rels)$

Metamath Proof Explorer