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	syl6bi	⊢ ( ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) = ( ◡ ◡ 𝑅 ∘ ◡ ◡ 𝑆 ) → ( ◡ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ ◡ 𝑇 → ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ) ) )
20	4 5 19	mpsyl	⊢ ( ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 → ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ) )
21	20	com12	⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 → ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ) )
22	3 21	impbid2	⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇 ) → ( ( 𝑅 ∘ 𝑆 ) ⊆ 𝑇 ↔ ( ◡ 𝑆 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑇 ) )