Metamath Proof Explorer

Theorem trclfv

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

Ref Expression
Assertion trclfv 
|- ( R e. V -> ( t+ ` R ) = |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( R e. V -> R e. _V )
2 trclexlem 
 |-  ( R e. _V -> ( R u. ( dom R X. ran R ) ) e. _V )
3 trclubg 
 |-  ( R e. _V -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } C_ ( R u. ( dom R X. ran R ) ) )
4 2 3 ssexd 
 |-  ( R e. _V -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } e. _V )
5 trcleq1 
 |-  ( r = R -> |^| { x | ( r C_ x /\ ( x o. x ) C_ x ) } = |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } )
6 df-trcl 
 |-  t+ = ( r e. _V |-> |^| { x | ( r C_ x /\ ( x o. x ) C_ x ) } )
7 5 6 fvmptg 
 |-  ( ( R e. _V /\ |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } e. _V ) -> ( t+ ` R ) = |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } )
8 1 4 7 syl2anc2 
 |-  ( R e. V -> ( t+ ` R ) = |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } )