Theorem dmtrclfv

Description: The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 9-May-2020)

	Ref	Expression
Assertion	dmtrclfv	|- ( R e. V -> dom ( t+ ` R ) = dom R )

Proof

Step	Hyp	Ref	Expression
1		trclfvub	|- ( R e. V -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )
2		dmss	|- ( ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) -> dom ( t+ ` R ) C_ dom ( R u. ( dom R X. ran R ) ) )
3	1 2	syl	|- ( R e. V -> dom ( t+ ` R ) C_ dom ( R u. ( dom R X. ran R ) ) )
4		dmun	|- dom ( R u. ( dom R X. ran R ) ) = ( dom R u. dom ( dom R X. ran R ) )
5		dm0rn0	|- ( dom R = (/) <-> ran R = (/) )
6		xpeq1	|- ( dom R = (/) -> ( dom R X. ran R ) = ( (/) X. ran R ) )
7		0xp	|- ( (/) X. ran R ) = (/)
8	6 7	eqtrdi	|- ( dom R = (/) -> ( dom R X. ran R ) = (/) )
9	8	dmeqd	|- ( dom R = (/) -> dom ( dom R X. ran R ) = dom (/) )
10		dm0	|- dom (/) = (/)
11	10	a1i	|- ( dom R = (/) -> dom (/) = (/) )
12		eqcom	|- ( dom R = (/) <-> (/) = dom R )
13	12	biimpi	|- ( dom R = (/) -> (/) = dom R )
14	9 11 13	3eqtrd	|- ( dom R = (/) -> dom ( dom R X. ran R ) = dom R )
15	5 14	sylbir	|- ( ran R = (/) -> dom ( dom R X. ran R ) = dom R )
16		dmxp	|- ( ran R =/= (/) -> dom ( dom R X. ran R ) = dom R )
17	15 16	pm2.61ine	|- dom ( dom R X. ran R ) = dom R
18	17	uneq2i	|- ( dom R u. dom ( dom R X. ran R ) ) = ( dom R u. dom R )
19		unidm	|- ( dom R u. dom R ) = dom R
20	4 18 19	3eqtri	|- dom ( R u. ( dom R X. ran R ) ) = dom R
21	3 20	sseqtrdi	|- ( R e. V -> dom ( t+ ` R ) C_ dom R )
22		trclfvlb	|- ( R e. V -> R C_ ( t+ ` R ) )
23		dmss	|- ( R C_ ( t+ ` R ) -> dom R C_ dom ( t+ ` R ) )
24	22 23	syl	|- ( R e. V -> dom R C_ dom ( t+ ` R ) )
25	21 24	eqssd	|- ( R e. V -> dom ( t+ ` R ) = dom R )