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	|- ( R e. V -> dom ( t+ ` R ) = dom R )

Proof

Step	Hyp	Ref	Expression
1		trclfvdecomr	|- ( R e. V -> ( t+ ` R ) = ( R u. ( ( t+ ` R ) o. R ) ) )
2	1	dmeqd	|- ( R e. V -> dom ( t+ ` R ) = dom ( R u. ( ( t+ ` R ) o. R ) ) )
3		dmun	|- dom ( R u. ( ( t+ ` R ) o. R ) ) = ( dom R u. dom ( ( t+ ` R ) o. R ) )
4		dmcoss	|- dom ( ( t+ ` R ) o. R ) C_ dom R
5		ssequn2	|- ( dom ( ( t+ ` R ) o. R ) C_ dom R <-> ( dom R u. dom ( ( t+ ` R ) o. R ) ) = dom R )
6	4 5	mpbi	|- ( dom R u. dom ( ( t+ ` R ) o. R ) ) = dom R
7	3 6	eqtri	|- dom ( R u. ( ( t+ ` R ) o. R ) ) = dom R
8	2 7	eqtrdi	|- ( R e. V -> dom ( t+ ` R ) = dom R )