Theorem dftrrel3

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

	Ref	Expression
Assertion	dftrrel3	|- ( TrRel R <-> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ Rel R ) )

Proof

Step	Hyp	Ref	Expression
1		dftrrel2	|- ( TrRel R <-> ( ( R o. R ) C_ R /\ Rel R ) )
2		cotr	|- ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
3	2	anbi1i	|- ( ( ( R o. R ) C_ R /\ Rel R ) <-> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ Rel R ) )
4	1 3	bitri	|- ( TrRel R <-> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ Rel R ) )