Metamath Proof Explorer

Theorem relcnvtrg

Description: General form of relcnvtr . (Contributed by Peter Mazsa, 17-Oct-2023)

Ref Expression
Assertion relcnvtrg ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ↔ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 cnvco ⊢ ◡ ( 𝑅 ∘ 𝑆 ) = ( ◡ 𝑆 ∘ ◡ 𝑅 )
2 cnvss ⊢ ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 → ◡ ( 𝑅 ∘ 𝑆 ) ⊆ ◡ 𝑇 )
3 1 2 eqsstrrid ⊢ ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 → ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 )
4 cnvco ⊢ ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) = ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 )
5 cnvss ⊢ ( ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 → ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ ◡ 𝑇 )
6 sseq1 ⊢ ( ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) = ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 ) → ( ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ ◡ 𝑇 ↔ ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 ) ⊆ ◡ ◡ 𝑇 ) )
7 dfrel2 ⊢ ( Rel 𝑅 ↔ ◡ ◡ 𝑅 = 𝑅 )
8 7 biimpi ⊢ ( Rel 𝑅 → ◡ ◡ 𝑅 = 𝑅 )
9 8 3ad2ant1 ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ◡ ◡ 𝑅 = 𝑅 )
10 dfrel2 ⊢ ( Rel 𝑆 ↔ ◡ ◡ 𝑆 = 𝑆 )
11 10 biimpi ⊢ ( Rel 𝑆 → ◡ ◡ 𝑆 = 𝑆 )
12 11 3ad2ant2 ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ◡ ◡ 𝑆 = 𝑆 )
13 9 12 coeq12d ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 ) = ( 𝑅 ∘ 𝑆 ) )
14 dfrel2 ⊢ ( Rel 𝑇 ↔ ◡ ◡ 𝑇 = 𝑇 )
15 14 biimpi ⊢ ( Rel 𝑇 → ◡ ◡ 𝑇 = 𝑇 )
16 15 3ad2ant3 ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ◡ ◡ 𝑇 = 𝑇 )
17 13 16 sseq12d ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 ) ⊆ ◡ ◡ 𝑇 ↔ ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ) )
18 17 biimpcd ⊢ ( ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 ) ⊆ ◡ ◡ 𝑇 → ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ) )
19 6 18 biimtrdi ⊢ ( ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) = ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 ) → ( ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ ◡ 𝑇 → ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ) ) )
20 4 5 19 mpsyl ⊢ ( ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 → ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ) )
21 20 com12 ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 → ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ) )
22 3 21 impbid2 ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ↔ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 ) )