Metamath Proof Explorer

Theorem trclfvlb2

Description: The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020)

Ref Expression
Assertion trclfvlb2 
|- ( R e. V -> ( R o. R ) C_ ( t+ ` R ) )

Proof

Step Hyp Ref Expression
1 trclfvcotr 
 |-  ( R e. V -> ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) )
2 trclfvlb 
 |-  ( R e. V -> R C_ ( t+ ` R ) )
3 1 2 2 trrelssd 
 |-  ( R e. V -> ( R o. R ) C_ ( t+ ` R ) )