Metamath Proof Explorer

Theorem trclfvlb3

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

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

Proof

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