Metamath Proof Explorer

Theorem cottrcl

Description: Composition law for the transitive closure of a relationship. (Contributed by Scott Fenton, 20-Oct-2024)

Ref Expression
Assertion cottrcl 
|- ( R o. t++ R ) C_ t++ R

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( R |` _V )
2 ssttrcl 
 |-  ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) )
3 1 2 ax-mp 
 |-  ( R |` _V ) C_ t++ ( R |` _V )
4 coss1 
 |-  ( ( R |` _V ) C_ t++ ( R |` _V ) -> ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) )
5 3 4 ax-mp 
 |-  ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) )
6 ttrcltr 
 |-  ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) C_ t++ ( R |` _V )
7 5 6 sstri 
 |-  ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ t++ ( R |` _V )
8 ssv 
 |-  ran t++ ( R |` _V ) C_ _V
9 cores 
 |-  ( ran t++ ( R |` _V ) C_ _V -> ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ ( R |` _V ) ) )
10 8 9 ax-mp 
 |-  ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ ( R |` _V ) )
11 ttrclresv 
 |-  t++ ( R |` _V ) = t++ R
12 11 coeq2i 
 |-  ( R o. t++ ( R |` _V ) ) = ( R o. t++ R )
13 10 12 eqtri 
 |-  ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ R )
14 7 13 11 3sstr3i 
 |-  ( R o. t++ R ) C_ t++ R