Description: The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | trclfvcom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex | |
|
2 | relexpsucnnr | |
|
3 | relexpsucnnl | |
|
4 | 2 3 | eqtr3d | |
5 | 4 | iuneq2dv | |
6 | oveq1 | |
|
7 | 6 | iuneq2d | |
8 | dftrcl3 | |
|
9 | nnex | |
|
10 | ovex | |
|
11 | 9 10 | iunex | |
12 | 7 8 11 | fvmpt | |
13 | 12 | coeq1d | |
14 | coiun1 | |
|
15 | 13 14 | eqtrdi | |
16 | 12 | coeq2d | |
17 | coiun | |
|
18 | 16 17 | eqtrdi | |
19 | 5 15 18 | 3eqtr4d | |
20 | 1 19 | syl | |