Description: The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 19-Jul-2020) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | rntrclfvRP | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rn | |
|
2 | cnvtrclfv | |
|
3 | 2 | dmeqd | |
4 | cnvexg | |
|
5 | dmtrclfv | |
|
6 | 4 5 | syl | |
7 | df-rn | |
|
8 | 6 7 | eqtr4di | |
9 | 3 8 | eqtrd | |
10 | 1 9 | eqtrid | |