Metamath Proof Explorer

Theorem relcnvtrg

Description: Subclass law for converse of a composition. A particular case is ( ( R o. R ) C_ R <-> (`' R o. ``' R ) C_ ``' R ) ` , which says that a relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011) Generalize to a statement about three classes rather than one. (Revised by Peter Mazsa, 17-Oct-2023) Remove antecedent. (Revised by Eric Schmidt, 8-Aug-2026)

Ref Expression
Assertion relcnvtrg 
|- ( ( R o. S ) C_ T <-> ( `' S o. `' R ) C_ `' T )

Proof

Step Hyp Ref Expression
1 cnvco 
 |-  `' ( R o. S ) = ( `' S o. `' R )
2 cnvss 
 |-  ( ( R o. S ) C_ T -> `' ( R o. S ) C_ `' T )
3 1 2 eqsstrrid 
 |-  ( ( R o. S ) C_ T -> ( `' S o. `' R ) C_ `' T )
4 cnvco 
 |-  `' ( `' S o. `' R ) = ( `' `' R o. `' `' S )
5 cocnvcnv1 
 |-  ( `' `' R o. `' `' S ) = ( R o. `' `' S )
6 cocnvcnv2 
 |-  ( R o. `' `' S ) = ( R o. S )
7 4 5 6 3eqtri 
 |-  `' ( `' S o. `' R ) = ( R o. S )
8 cnvss 
 |-  ( ( `' S o. `' R ) C_ `' T -> `' ( `' S o. `' R ) C_ `' `' T )
9 7 8 eqsstrrid 
 |-  ( ( `' S o. `' R ) C_ `' T -> ( R o. S ) C_ `' `' T )
10 cnvcnvss 
 |-  `' `' T C_ T
11 9 10 sstrdi 
 |-  ( ( `' S o. `' R ) C_ `' T -> ( R o. S ) C_ T )
12 3 11 impbii 
 |-  ( ( R o. S ) C_ T <-> ( `' S o. `' R ) C_ `' T )