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	⊢ ( 𝑅 ∈ 𝑉 → ran ( t+ ‘ 𝑅 ) = ran 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran ( t+ ‘ 𝑅 ) = dom ◡ ( t+ ‘ 𝑅 )
2		cnvtrclfv	⊢ ( 𝑅 ∈ 𝑉 → ◡ ( t+ ‘ 𝑅 ) = ( t+ ‘ ◡ 𝑅 ) )
3	2	dmeqd	⊢ ( 𝑅 ∈ 𝑉 → dom ◡ ( t+ ‘ 𝑅 ) = dom ( t+ ‘ ◡ 𝑅 ) )
4		cnvexg	⊢ ( 𝑅 ∈ 𝑉 → ◡ 𝑅 ∈ V )
5		dmtrclfv	⊢ ( ◡ 𝑅 ∈ V → dom ( t+ ‘ ◡ 𝑅 ) = dom ◡ 𝑅 )
6	4 5	syl	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ ◡ 𝑅 ) = dom ◡ 𝑅 )
7		df-rn	⊢ ran 𝑅 = dom ◡ 𝑅
8	6 7	eqtr4di	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ ◡ 𝑅 ) = ran 𝑅 )
9	3 8	eqtrd	⊢ ( 𝑅 ∈ 𝑉 → dom ◡ ( t+ ‘ 𝑅 ) = ran 𝑅 )
10	1 9	syl5eq	⊢ ( 𝑅 ∈ 𝑉 → ran ( t+ ‘ 𝑅 ) = ran 𝑅 )