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\in V\to \mathrm{ran}\mathrm{t+}\left(R\right)=\mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}\mathrm{t+}\left(R\right)=\mathrm{dom}{\mathrm{t+}\left(R\right)}^{-1}$$
2		cnvtrclfv	$$⊢R\in V\to {\mathrm{t+}\left(R\right)}^{-1}=\mathrm{t+}\left(R^{-1}\right)$$
3	2	dmeqd	$$⊢R\in V\to \mathrm{dom}{\mathrm{t+}\left(R\right)}^{-1}=\mathrm{dom}\mathrm{t+}\left(R^{-1}\right)$$
4		cnvexg	$$⊢R\in V\to R^{-1}\in \mathrm{V}$$
5		dmtrclfv	$$⊢R^{-1}\in \mathrm{V}\to \mathrm{dom}\mathrm{t+}\left(R^{-1}\right)=\mathrm{dom}{R}^{-1}$$
6	4 5	syl	$$⊢R\in V\to \mathrm{dom}\mathrm{t+}\left(R^{-1}\right)=\mathrm{dom}{R}^{-1}$$
7		df-rn	$$⊢\mathrm{ran}R=\mathrm{dom}{R}^{-1}$$
8	6 7	eqtr4di	$$⊢R\in V\to \mathrm{dom}\mathrm{t+}\left(R^{-1}\right)=\mathrm{ran}R$$
9	3 8	eqtrd	$$⊢R\in V\to \mathrm{dom}{\mathrm{t+}\left(R\right)}^{-1}=\mathrm{ran}R$$
10	1 9	syl5eq	$$⊢R\in V\to \mathrm{ran}\mathrm{t+}\left(R\right)=\mathrm{ran}R$$