Theorem cotr2

Description: Two ways of saying a relation is transitive. Special instance of cotr2g . (Contributed by RP, 22-Mar-2020)

	Ref	Expression
Hypotheses	cotr2.a	|- dom R C_ A
	cotr2.b	|- ( dom R i^i ran R ) C_ B
	cotr2.c	|- ran R C_ C
Assertion	cotr2	|- ( ( R o. R ) C_ R <-> A. x e. A A. y e. B A. z e. C ( ( x R y /\ y R z ) -> x R z ) )

Proof

Step	Hyp	Ref	Expression
1		cotr2.a	|- dom R C_ A
2		cotr2.b	|- ( dom R i^i ran R ) C_ B
3		cotr2.c	|- ran R C_ C
4		incom	|- ( dom R i^i ran R ) = ( ran R i^i dom R )
5	4 2	eqsstrri	|- ( ran R i^i dom R ) C_ B
6	1 5 3	cotr2g	|- ( ( R o. R ) C_ R <-> A. x e. A A. y e. B A. z e. C ( ( x R y /\ y R z ) -> x R z ) )