Theorem rntrclfv

Description: The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 18-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	rntrclfv	|- ( R e. V -> ran ( t+ ` R ) = ran R )

Proof

Step	Hyp	Ref	Expression
1		trclfvdecoml	|- ( R e. V -> ( t+ ` R ) = ( R u. ( R o. ( t+ ` R ) ) ) )
2	1	rneqd	|- ( R e. V -> ran ( t+ ` R ) = ran ( R u. ( R o. ( t+ ` R ) ) ) )
3		rnun	|- ran ( R u. ( R o. ( t+ ` R ) ) ) = ( ran R u. ran ( R o. ( t+ ` R ) ) )
4		rncoss	|- ran ( R o. ( t+ ` R ) ) C_ ran R
5		ssequn2	|- ( ran ( R o. ( t+ ` R ) ) C_ ran R <-> ( ran R u. ran ( R o. ( t+ ` R ) ) ) = ran R )
6	4 5	mpbi	|- ( ran R u. ran ( R o. ( t+ ` R ) ) ) = ran R
7	3 6	eqtri	|- ran ( R u. ( R o. ( t+ ` R ) ) ) = ran R
8	2 7	eqtrdi	|- ( R e. V -> ran ( t+ ` R ) = ran R )