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	⊢ ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ↔ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		cnvco	⊢ ◡ ( 𝑅 ∘ 𝑆 ) = ( ◡ 𝑆 ∘ ◡ 𝑅 )
2		cnvss	⊢ ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 → ◡ ( 𝑅 ∘ 𝑆 ) ⊆ ◡ 𝑇 )
3	1 2	eqsstrrid	⊢ ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 → ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 )
4		cnvco	⊢ ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) = ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 )
5		cocnvcnv1	⊢ ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 ) = ( 𝑅 ∘ ◡ ◡ 𝑆 )
6		cocnvcnv2	⊢ ( 𝑅 ∘ ◡ ◡ 𝑆 ) = ( 𝑅 ∘ 𝑆 )
7	4 5 6	3eqtri	⊢ ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) = ( 𝑅 ∘ 𝑆 )
8		cnvss	⊢ ( ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 → ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ ◡ 𝑇 )
9	7 8	eqsstrrid	⊢ ( ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 → ( 𝑅 ∘ 𝑆 ) ⊆ ◡ ◡ 𝑇 )
10		cnvcnvss	⊢ ◡ ◡ 𝑇 ⊆ 𝑇
11	9 10	sstrdi	⊢ ( ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 → ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 )
12	3 11	impbii	⊢ ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ↔ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 )