Theorem relcnvtr

Description: A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011) (Proof shortened by Peter Mazsa, 17-Oct-2023)

	Ref	Expression
Assertion	relcnvtr	|- ( Rel R -> ( ( R o. R ) C_ R <-> ( `' R o. `' R ) C_ `' R ) )

Proof

Step	Hyp	Ref	Expression
1		3anidm	|- ( ( Rel R /\ Rel R /\ Rel R ) <-> Rel R )
2		relcnvtrg	|- ( ( Rel R /\ Rel R /\ Rel R ) -> ( ( R o. R ) C_ R <-> ( `' R o. `' R ) C_ `' R ) )
3	1 2	sylbir	|- ( Rel R -> ( ( R o. R ) C_ R <-> ( `' R o. `' R ) C_ `' R ) )