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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex | |
|
2 | nnnn0 | |
|
3 | relexpcnv | |
|
4 | 2 3 | sylan | |
5 | 4 | expcom | |
6 | 5 | ralrimiv | |
7 | iuneq2 | |
|
8 | 6 7 | syl | |
9 | oveq1 | |
|
10 | 9 | iuneq2d | |
11 | dftrcl3 | |
|
12 | nnex | |
|
13 | ovex | |
|
14 | 12 13 | iunex | |
15 | 10 11 14 | fvmpt | |
16 | 15 | cnveqd | |
17 | cnviun | |
|
18 | 16 17 | eqtrdi | |
19 | cnvexg | |
|
20 | oveq1 | |
|
21 | 20 | iuneq2d | |
22 | dftrcl3 | |
|
23 | ovex | |
|
24 | 12 23 | iunex | |
25 | 21 22 24 | fvmpt | |
26 | 19 25 | syl | |
27 | 8 18 26 | 3eqtr4d | |
28 | 1 27 | syl | |