Theorem cnvtrrel

Description: The converse of a transitive relation is a transitive relation. (Contributed by RP, 25-Dec-2019)

	Ref	Expression
Assertion	cnvtrrel	|- ( ( S o. S ) C_ S <-> ( `' S o. `' S ) C_ `' S )

Proof

Step	Hyp	Ref	Expression
1		cnvss	|- ( ( S o. S ) C_ S -> `' ( S o. S ) C_ `' S )
2		cnvss	|- ( `' ( S o. S ) C_ `' S -> `' `' ( S o. S ) C_ `' `' S )
3		cnvco	|- `' ( S o. S ) = ( `' S o. `' S )
4	3	cnveqi	|- `' `' ( S o. S ) = `' ( `' S o. `' S )
5		cnvco	|- `' ( `' S o. `' S ) = ( `' `' S o. `' `' S )
6		cocnvcnv1	|- ( `' `' S o. `' `' S ) = ( S o. `' `' S )
7		cocnvcnv2	|- ( S o. `' `' S ) = ( S o. S )
8	6 7	eqtri	|- ( `' `' S o. `' `' S ) = ( S o. S )
9	4 5 8	3eqtri	|- `' `' ( S o. S ) = ( S o. S )
10	9	sseq1i	|- ( `' `' ( S o. S ) C_ `' `' S <-> ( S o. S ) C_ `' `' S )
11	10	biimpi	|- ( `' `' ( S o. S ) C_ `' `' S -> ( S o. S ) C_ `' `' S )
12		cnvcnvss	|- `' `' S C_ S
13	11 12	sstrdi	|- ( `' `' ( S o. S ) C_ `' `' S -> ( S o. S ) C_ S )
14	2 13	syl	|- ( `' ( S o. S ) C_ `' S -> ( S o. S ) C_ S )
15	1 14	impbii	|- ( ( S o. S ) C_ S <-> `' ( S o. S ) C_ `' S )
16	3	sseq1i	|- ( `' ( S o. S ) C_ `' S <-> ( `' S o. `' S ) C_ `' S )
17	15 16	bitri	|- ( ( S o. S ) C_ S <-> ( `' S o. `' S ) C_ `' S )