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	|- ( R e. V -> ran ( t+ ` R ) = ran R )

Proof

Step	Hyp	Ref	Expression
1		df-rn	|- ran ( t+ ` R ) = dom `' ( t+ ` R )
2		cnvtrclfv	|- ( R e. V -> `' ( t+ ` R ) = ( t+ ` `' R ) )
3	2	dmeqd	|- ( R e. V -> dom `' ( t+ ` R ) = dom ( t+ ` `' R ) )
4		cnvexg	|- ( R e. V -> `' R e. _V )
5		dmtrclfv	|- ( `' R e. _V -> dom ( t+ ` `' R ) = dom `' R )
6	4 5	syl	|- ( R e. V -> dom ( t+ ` `' R ) = dom `' R )
7		df-rn	|- ran R = dom `' R
8	6 7	eqtr4di	|- ( R e. V -> dom ( t+ ` `' R ) = ran R )
9	3 8	eqtrd	|- ( R e. V -> dom `' ( t+ ` R ) = ran R )
10	1 9	eqtrid	|- ( R e. V -> ran ( t+ ` R ) = ran R )