Metamath Proof Explorer


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 RVdomt+R=domR

Proof

Step Hyp Ref Expression
1 trclfvub RVt+RRdomR×ranR
2 dmss t+RRdomR×ranRdomt+RdomRdomR×ranR
3 1 2 syl RVdomt+RdomRdomR×ranR
4 dmun domRdomR×ranR=domRdomdomR×ranR
5 dm0rn0 domR=ranR=
6 xpeq1 domR=domR×ranR=×ranR
7 0xp ×ranR=
8 6 7 eqtrdi domR=domR×ranR=
9 8 dmeqd domR=domdomR×ranR=dom
10 dm0 dom=
11 10 a1i domR=dom=
12 eqcom domR==domR
13 12 biimpi domR==domR
14 9 11 13 3eqtrd domR=domdomR×ranR=domR
15 5 14 sylbir ranR=domdomR×ranR=domR
16 dmxp ranRdomdomR×ranR=domR
17 15 16 pm2.61ine domdomR×ranR=domR
18 17 uneq2i domRdomdomR×ranR=domRdomR
19 unidm domRdomR=domR
20 4 18 19 3eqtri domRdomR×ranR=domR
21 3 20 sseqtrdi RVdomt+RdomR
22 trclfvlb RVRt+R
23 dmss Rt+RdomRdomt+R
24 22 23 syl RVdomRdomt+R
25 21 24 eqssd RVdomt+R=domR