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 RVt+RR=Rt+R

Proof

Step Hyp Ref Expression
1 elex RVRV
2 relexpsucnnr RVnRrn+1=RrnR
3 relexpsucnnl RVnRrn+1=RRrn
4 2 3 eqtr3d RVnRrnR=RRrn
5 4 iuneq2dv RVnRrnR=nRRrn
6 oveq1 r=Rrrn=Rrn
7 6 iuneq2d r=Rnrrn=nRrn
8 dftrcl3 t+=rVnrrn
9 nnex V
10 ovex RrnV
11 9 10 iunex nRrnV
12 7 8 11 fvmpt RVt+R=nRrn
13 12 coeq1d RVt+RR=nRrnR
14 coiun1 nRrnR=nRrnR
15 13 14 eqtrdi RVt+RR=nRrnR
16 12 coeq2d RVRt+R=RnRrn
17 coiun RnRrn=nRRrn
18 16 17 eqtrdi RVRt+R=nRRrn
19 5 15 18 3eqtr4d RVt+RR=Rt+R
20 1 19 syl RVt+RR=Rt+R