Metamath Proof Explorer

Theorem cnvtrrel

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

Ref Expression
Assertion cnvtrrel ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ↔ ( ◡ 𝑆 ∘ ◡ 𝑆 ) ⊆ ◡ 𝑆 )

Proof

Step Hyp Ref Expression
1 cnvss ⊢ ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 → ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ 𝑆 )
2 cnvss ⊢ ( ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ 𝑆 → ◡ ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ ◡ 𝑆 )
3 cnvco ⊢ ◡ ( 𝑆 ∘ 𝑆 ) = ( ◡ 𝑆 ∘ ◡ 𝑆 )
4 3 cnveqi ⊢ ◡ ◡ ( 𝑆 ∘ 𝑆 ) = ◡ ( ◡ 𝑆 ∘ ◡ 𝑆 )
5 cnvco ⊢ ◡ ( ◡ 𝑆 ∘ ◡ 𝑆 ) = ( ◡ ◡ 𝑆 ∘ ◡ ◡ 𝑆 )
6 cocnvcnv1 ⊢ ( ◡ ◡ 𝑆 ∘ ◡ ◡ 𝑆 ) = ( 𝑆 ∘ ◡ ◡ 𝑆 )
7 cocnvcnv2 ⊢ ( 𝑆 ∘ ◡ ◡ 𝑆 ) = ( 𝑆 ∘ 𝑆 )
8 6 7 eqtri ⊢ ( ◡ ◡ 𝑆 ∘ ◡ ◡ 𝑆 ) = ( 𝑆 ∘ 𝑆 )
9 4 5 8 3eqtri ⊢ ◡ ◡ ( 𝑆 ∘ 𝑆 ) = ( 𝑆 ∘ 𝑆 )
10 9 sseq1i ⊢ ( ◡ ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ ◡ 𝑆 ↔ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ ◡ 𝑆 )
11 10 biimpi ⊢ ( ◡ ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ ◡ 𝑆 → ( 𝑆 ∘ 𝑆 ) ⊆ ◡ ◡ 𝑆 )
12 cnvcnvss ⊢ ◡ ◡ 𝑆 ⊆ 𝑆
13 11 12 sstrdi ⊢ ( ◡ ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ ◡ 𝑆 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )
14 2 13 syl ⊢ ( ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ 𝑆 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )
15 1 14 impbii ⊢ ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ↔ ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ 𝑆 )
16 3 sseq1i ⊢ ( ◡ ( 𝑆 ∘ 𝑆 ) ⊆ ◡ 𝑆 ↔ ( ◡ 𝑆 ∘ ◡ 𝑆 ) ⊆ ◡ 𝑆 )
17 15 16 bitri ⊢ ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ↔ ( ◡ 𝑆 ∘ ◡ 𝑆 ) ⊆ ◡ 𝑆 )