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