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

Proof

Step	Hyp	Ref	Expression
1		trclfvdecoml	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ( 𝑅 ∪ ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) )
2	1	rneqd	⊢ ( 𝑅 ∈ 𝑉 → ran ( t+ ‘ 𝑅 ) = ran ( 𝑅 ∪ ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) )
3		rnun	⊢ ran ( 𝑅 ∪ ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) = ( ran 𝑅 ∪ ran ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) )
4		rncoss	⊢ ran ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ran 𝑅
5		ssequn2	⊢ ( ran ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ran 𝑅 ↔ ( ran 𝑅 ∪ ran ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) = ran 𝑅 )
6	4 5	mpbi	⊢ ( ran 𝑅 ∪ ran ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) = ran 𝑅
7	3 6	eqtri	⊢ ran ( 𝑅 ∪ ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) = ran 𝑅
8	2 7	eqtrdi	⊢ ( 𝑅 ∈ 𝑉 → ran ( t+ ‘ 𝑅 ) = ran 𝑅 )