Metamath Proof Explorer

Theorem relcnvtrg

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

Ref Expression
Assertion relcnvtrg ⊢ Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → R ∘ S ⊆ T ↔ S -1 ∘ R -1 ⊆ T -1

Proof

Step Hyp Ref Expression
1 cnvco ⊢ R ∘ S -1 = S -1 ∘ R -1
2 cnvss ⊢ R ∘ S ⊆ T → R ∘ S -1 ⊆ T -1
3 1 2 eqsstrrid ⊢ R ∘ S ⊆ T → S -1 ∘ R -1 ⊆ T -1
4 cnvco ⊢ S -1 ∘ R -1 -1 = R -1 -1 ∘ S -1 -1
5 cnvss ⊢ S -1 ∘ R -1 ⊆ T -1 → S -1 ∘ R -1 -1 ⊆ T -1 -1
6 sseq1 ⊢ S -1 ∘ R -1 -1 = R -1 -1 ∘ S -1 -1 → S -1 ∘ R -1 -1 ⊆ T -1 -1 ↔ R -1 -1 ∘ S -1 -1 ⊆ T -1 -1
7 dfrel2 ⊢ Rel ⁡ R ↔ R -1 -1 = R
8 7 biimpi ⊢ Rel ⁡ R → R -1 -1 = R
9 8 3ad2ant1 ⊢ Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → R -1 -1 = R
10 dfrel2 ⊢ Rel ⁡ S ↔ S -1 -1 = S
11 10 biimpi ⊢ Rel ⁡ S → S -1 -1 = S
12 11 3ad2ant2 ⊢ Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → S -1 -1 = S
13 9 12 coeq12d ⊢ Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → R -1 -1 ∘ S -1 -1 = R ∘ S
14 dfrel2 ⊢ Rel ⁡ T ↔ T -1 -1 = T
15 14 biimpi ⊢ Rel ⁡ T → T -1 -1 = T
16 15 3ad2ant3 ⊢ Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → T -1 -1 = T
17 13 16 sseq12d ⊢ Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → R -1 -1 ∘ S -1 -1 ⊆ T -1 -1 ↔ R ∘ S ⊆ T
18 17 biimpcd ⊢ R -1 -1 ∘ S -1 -1 ⊆ T -1 -1 → Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → R ∘ S ⊆ T
19 6 18 syl6bi ⊢ S -1 ∘ R -1 -1 = R -1 -1 ∘ S -1 -1 → S -1 ∘ R -1 -1 ⊆ T -1 -1 → Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → R ∘ S ⊆ T
20 4 5 19 mpsyl ⊢ S -1 ∘ R -1 ⊆ T -1 → Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → R ∘ S ⊆ T
21 20 com12 ⊢ Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → S -1 ∘ R -1 ⊆ T -1 → R ∘ S ⊆ T
22 3 21 impbid2 ⊢ Rel ⁡ R ∧ Rel ⁡ S ∧ Rel ⁡ T → R ∘ S ⊆ T ↔ S -1 ∘ R -1 ⊆ T -1