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 o. S ) C_ T <-> ( `' S o. `' R ) C_ `' T ) )

Proof

Step Hyp Ref Expression
1 cnvco 
 |-  `' ( R o. S ) = ( `' S o. `' R )
2 cnvss 
 |-  ( ( R o. S ) C_ T -> `' ( R o. S ) C_ `' T )
3 1 2 eqsstrrid 
 |-  ( ( R o. S ) C_ T -> ( `' S o. `' R ) C_ `' T )
4 cnvco 
 |-  `' ( `' S o. `' R ) = ( `' `' R o. `' `' S )
5 cnvss 
 |-  ( ( `' S o. `' R ) C_ `' T -> `' ( `' S o. `' R ) C_ `' `' T )
6 sseq1 
 |-  ( `' ( `' S o. `' R ) = ( `' `' R o. `' `' S ) -> ( `' ( `' S o. `' R ) C_ `' `' T <-> ( `' `' R o. `' `' S ) C_ `' `' T ) )
7 dfrel2 
 |-  ( Rel R <-> `' `' R = R )
8 7 biimpi 
 |-  ( Rel R -> `' `' R = R )
9 8 3ad2ant1 
 |-  ( ( Rel R /\ Rel S /\ Rel T ) -> `' `' R = R )
10 dfrel2 
 |-  ( Rel S <-> `' `' S = S )
11 10 biimpi 
 |-  ( Rel S -> `' `' S = S )
12 11 3ad2ant2 
 |-  ( ( Rel R /\ Rel S /\ Rel T ) -> `' `' S = S )
13 9 12 coeq12d 
 |-  ( ( Rel R /\ Rel S /\ Rel T ) -> ( `' `' R o. `' `' S ) = ( R o. S ) )
14 dfrel2 
 |-  ( Rel T <-> `' `' T = T )
15 14 biimpi 
 |-  ( Rel T -> `' `' T = T )
16 15 3ad2ant3 
 |-  ( ( Rel R /\ Rel S /\ Rel T ) -> `' `' T = T )
17 13 16 sseq12d 
 |-  ( ( Rel R /\ Rel S /\ Rel T ) -> ( ( `' `' R o. `' `' S ) C_ `' `' T <-> ( R o. S ) C_ T ) )
18 17 biimpcd 
 |-  ( ( `' `' R o. `' `' S ) C_ `' `' T -> ( ( Rel R /\ Rel S /\ Rel T ) -> ( R o. S ) C_ T ) )
19 6 18 syl6bi 
 |-  ( `' ( `' S o. `' R ) = ( `' `' R o. `' `' S ) -> ( `' ( `' S o. `' R ) C_ `' `' T -> ( ( Rel R /\ Rel S /\ Rel T ) -> ( R o. S ) C_ T ) ) )
20 4 5 19 mpsyl 
 |-  ( ( `' S o. `' R ) C_ `' T -> ( ( Rel R /\ Rel S /\ Rel T ) -> ( R o. S ) C_ T ) )
21 20 com12 
 |-  ( ( Rel R /\ Rel S /\ Rel T ) -> ( ( `' S o. `' R ) C_ `' T -> ( R o. S ) C_ T ) )
22 3 21 impbid2 
 |-  ( ( Rel R /\ Rel S /\ Rel T ) -> ( ( R o. S ) C_ T <-> ( `' S o. `' R ) C_ `' T ) )