Theorem dmtrclfvRP

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

	Ref	Expression
Assertion	dmtrclfvRP	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ 𝑅 ) = dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		trclfvdecomr	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) )
2	1	dmeqd	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ 𝑅 ) = dom ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) )
3		dmun	⊢ dom ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) = ( dom 𝑅 ∪ dom ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) )
4		dmcoss	⊢ dom ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ⊆ dom 𝑅
5		ssequn2	⊢ ( dom ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ⊆ dom 𝑅 ↔ ( dom 𝑅 ∪ dom ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) = dom 𝑅 )
6	4 5	mpbi	⊢ ( dom 𝑅 ∪ dom ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) = dom 𝑅
7	3 6	eqtri	⊢ dom ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) = dom 𝑅
8	2 7	eqtrdi	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ 𝑅 ) = dom 𝑅 )