Metamath Proof Explorer

Theorem ttrclco

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

Ref Expression
Assertion ttrclco 
|- ( t++ R o. 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 coss2 
 |-  ( ( R |` _V ) C_ t++ ( R |` _V ) -> ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) )
4 1 2 3 mp2b 
 |-  ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) )
5 ttrcltr 
 |-  ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) C_ t++ ( R |` _V )
6 4 5 sstri 
 |-  ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ t++ ( R |` _V )
7 relco 
 |-  Rel ( t++ ( R |` _V ) o. R )
8 dfrel3 
 |-  ( Rel ( t++ ( R |` _V ) o. R ) <-> ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. R ) )
9 7 8 mpbi 
 |-  ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. R )
10 resco 
 |-  ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. ( R |` _V ) )
11 ttrclresv 
 |-  t++ ( R |` _V ) = t++ R
12 11 coeq1i 
 |-  ( t++ ( R |` _V ) o. R ) = ( t++ R o. R )
13 9 10 12 3eqtr3i 
 |-  ( t++ ( R |` _V ) o. ( R |` _V ) ) = ( t++ R o. R )
14 6 13 11 3sstr3i 
 |-  ( t++ R o. R ) C_ t++ R