Metamath Proof Explorer


Theorem rntrclfvRP

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 RVrant+R=ranR

Proof

Step Hyp Ref Expression
1 df-rn rant+R=domt+R-1
2 cnvtrclfv RVt+R-1=t+R-1
3 2 dmeqd RVdomt+R-1=domt+R-1
4 cnvexg RVR-1V
5 dmtrclfv R-1Vdomt+R-1=domR-1
6 4 5 syl RVdomt+R-1=domR-1
7 df-rn ranR=domR-1
8 6 7 eqtr4di RVdomt+R-1=ranR
9 3 8 eqtrd RVdomt+R-1=ranR
10 1 9 eqtrid RVrant+R=ranR