Theorem cotr3

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

	Ref	Expression
Hypotheses	cotr3.a	|- A = dom R
	cotr3.b	|- B = ( A i^i C )
	cotr3.c	|- C = ran R
Assertion	cotr3	|- ( ( 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		cotr3.a	|- A = dom R
2		cotr3.b	|- B = ( A i^i C )
3		cotr3.c	|- C = ran R
4	1	eqimss2i	|- dom R C_ A
5	1 3	ineq12i	|- ( A i^i C ) = ( dom R i^i ran R )
6	2 5	eqtri	|- B = ( dom R i^i ran R )
7	6	eqimss2i	|- ( dom R i^i ran R ) C_ B
8	3	eqimss2i	|- ran R C_ C
9	4 7 8	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 ) )