Metamath Proof Explorer

Theorem trclfvcotrg

Description: The value of the transitive closure of a relation is always a transitive relation. (Contributed by RP, 8-May-2020)

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

Proof

Step Hyp Ref Expression
1 trclfvcotr 
 |-  ( R e. _V -> ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) )
2 fvprc 
 |-  ( -. R e. _V -> ( t+ ` R ) = (/) )
3 0trrel 
 |-  ( (/) o. (/) ) C_ (/)
4 3 a1i 
 |-  ( ( t+ ` R ) = (/) -> ( (/) o. (/) ) C_ (/) )
5 id 
 |-  ( ( t+ ` R ) = (/) -> ( t+ ` R ) = (/) )
6 5 5 coeq12d 
 |-  ( ( t+ ` R ) = (/) -> ( ( t+ ` R ) o. ( t+ ` R ) ) = ( (/) o. (/) ) )
7 4 6 5 3sstr4d 
 |-  ( ( t+ ` R ) = (/) -> ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) )
8 2 7 syl 
 |-  ( -. R e. _V -> ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) )
9 1 8 pm2.61i 
 |-  ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R )