Metamath Proof Explorer


Theorem cnvtrclfv

Description: The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020)

Ref Expression
Assertion cnvtrclfv RVt+R-1=t+R-1

Proof

Step Hyp Ref Expression
1 elex RVRV
2 nnnn0 nn0
3 relexpcnv n0RVRrn-1=R-1rn
4 2 3 sylan nRVRrn-1=R-1rn
5 4 expcom RVnRrn-1=R-1rn
6 5 ralrimiv RVnRrn-1=R-1rn
7 iuneq2 nRrn-1=R-1rnnRrn-1=nR-1rn
8 6 7 syl RVnRrn-1=nR-1rn
9 oveq1 r=Rrrn=Rrn
10 9 iuneq2d r=Rnrrn=nRrn
11 dftrcl3 t+=rVnrrn
12 nnex V
13 ovex RrnV
14 12 13 iunex nRrnV
15 10 11 14 fvmpt RVt+R=nRrn
16 15 cnveqd RVt+R-1=nRrn-1
17 cnviun nRrn-1=nRrn-1
18 16 17 eqtrdi RVt+R-1=nRrn-1
19 cnvexg RVR-1V
20 oveq1 s=R-1srn=R-1rn
21 20 iuneq2d s=R-1nsrn=nR-1rn
22 dftrcl3 t+=sVnsrn
23 ovex R-1rnV
24 12 23 iunex nR-1rnV
25 21 22 24 fvmpt R-1Vt+R-1=nR-1rn
26 19 25 syl RVt+R-1=nR-1rn
27 8 18 26 3eqtr4d RVt+R-1=t+R-1
28 1 27 syl RVt+R-1=t+R-1