Metamath Proof Explorer

Theorem trclfvcom

Description: The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( R e. V -> R e. _V )
2 relexpsucnnr 
 |-  ( ( R e. _V /\ n e. NN ) -> ( R ^r ( n + 1 ) ) = ( ( R ^r n ) o. R ) )
3 relexpsucnnl 
 |-  ( ( R e. _V /\ n e. NN ) -> ( R ^r ( n + 1 ) ) = ( R o. ( R ^r n ) ) )
4 2 3 eqtr3d 
 |-  ( ( R e. _V /\ n e. NN ) -> ( ( R ^r n ) o. R ) = ( R o. ( R ^r n ) ) )
5 4 iuneq2dv 
 |-  ( R e. _V -> U_ n e. NN ( ( R ^r n ) o. R ) = U_ n e. NN ( R o. ( R ^r n ) ) )
6 oveq1 
 |-  ( r = R -> ( r ^r n ) = ( R ^r n ) )
7 6 iuneq2d 
 |-  ( r = R -> U_ n e. NN ( r ^r n ) = U_ n e. NN ( R ^r n ) )
8 dftrcl3 
 |-  t+ = ( r e. _V |-> U_ n e. NN ( r ^r n ) )
9 nnex 
 |-  NN e. _V
10 ovex 
 |-  ( R ^r n ) e. _V
11 9 10 iunex 
 |-  U_ n e. NN ( R ^r n ) e. _V
12 7 8 11 fvmpt 
 |-  ( R e. _V -> ( t+ ` R ) = U_ n e. NN ( R ^r n ) )
13 12 coeq1d 
 |-  ( R e. _V -> ( ( t+ ` R ) o. R ) = ( U_ n e. NN ( R ^r n ) o. R ) )
14 coiun1 
 |-  ( U_ n e. NN ( R ^r n ) o. R ) = U_ n e. NN ( ( R ^r n ) o. R )
15 13 14 eqtrdi 
 |-  ( R e. _V -> ( ( t+ ` R ) o. R ) = U_ n e. NN ( ( R ^r n ) o. R ) )
16 12 coeq2d 
 |-  ( R e. _V -> ( R o. ( t+ ` R ) ) = ( R o. U_ n e. NN ( R ^r n ) ) )
17 coiun 
 |-  ( R o. U_ n e. NN ( R ^r n ) ) = U_ n e. NN ( R o. ( R ^r n ) )
18 16 17 eqtrdi 
 |-  ( R e. _V -> ( R o. ( t+ ` R ) ) = U_ n e. NN ( R o. ( R ^r n ) ) )
19 5 15 18 3eqtr4d 
 |-  ( R e. _V -> ( ( t+ ` R ) o. R ) = ( R o. ( t+ ` R ) ) )
20 1 19 syl 
 |-  ( R e. V -> ( ( t+ ` R ) o. R ) = ( R o. ( t+ ` R ) ) )