dftrrel3

Description: Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021)

		Ref	Expression
	Assertion	dftrrel3	$⊢ TrRel R \leftrightarrow (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land Rel R)$

Step	Hyp	Ref	Expression
1		dftrrel2	$⊢ TrRel R \leftrightarrow (R \circ R \subseteq R \land Rel R)$
2		cotr	$⊢ R \circ R \subseteq R \leftrightarrow \forall x \forall y \forall z ((x R y \land y R z) \to x R z)$
3	2	anbi1i	$⊢ (R \circ R \subseteq R \land Rel R) \leftrightarrow (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land Rel R)$
4	1 3	bitri	$⊢ TrRel R \leftrightarrow (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land Rel R)$

Metamath Proof Explorer