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 R V t+ R -1 = t+ R -1

Proof

Step Hyp Ref Expression
1 elex R V R V
2 nnnn0 n n 0
3 relexpcnv n 0 R V R r n -1 = R -1 r n
4 2 3 sylan n R V R r n -1 = R -1 r n
5 4 expcom R V n R r n -1 = R -1 r n
6 5 ralrimiv R V n R r n -1 = R -1 r n
7 iuneq2 n R r n -1 = R -1 r n n R r n -1 = n R -1 r n
8 6 7 syl R V n R r n -1 = n R -1 r n
9 oveq1 r = R r r n = R r n
10 9 iuneq2d r = R n r r n = n R r n
11 dftrcl3 t+ = r V n r r n
12 nnex V
13 ovex R r n V
14 12 13 iunex n R r n V
15 10 11 14 fvmpt R V t+ R = n R r n
16 15 cnveqd R V t+ R -1 = n R r n -1
17 cnviun n R r n -1 = n R r n -1
18 16 17 eqtrdi R V t+ R -1 = n R r n -1
19 cnvexg R V R -1 V
20 oveq1 s = R -1 s r n = R -1 r n
21 20 iuneq2d s = R -1 n s r n = n R -1 r n
22 dftrcl3 t+ = s V n s r n
23 ovex R -1 r n V
24 12 23 iunex n R -1 r n V
25 21 22 24 fvmpt R -1 V t+ R -1 = n R -1 r n
26 19 25 syl R V t+ R -1 = n R -1 r n
27 8 18 26 3eqtr4d R V t+ R -1 = t+ R -1
28 1 27 syl R V t+ R -1 = t+ R -1