Metamath Proof Explorer

Theorem trclfvlb

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

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

Proof

Step Hyp Ref Expression
1 ssmin 
 |-  R C_ |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) }
2 trclfv 
 |-  ( R e. V -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
3 1 2 sseqtrrid 
 |-  ( R e. V -> R C_ ( t+ ` R ) )