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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trclfvub | |
|
2 | dmss | |
|
3 | 1 2 | syl | |
4 | dmun | |
|
5 | dm0rn0 | |
|
6 | xpeq1 | |
|
7 | 0xp | |
|
8 | 6 7 | eqtrdi | |
9 | 8 | dmeqd | |
10 | dm0 | |
|
11 | 10 | a1i | |
12 | eqcom | |
|
13 | 12 | biimpi | |
14 | 9 11 13 | 3eqtrd | |
15 | 5 14 | sylbir | |
16 | dmxp | |
|
17 | 15 16 | pm2.61ine | |
18 | 17 | uneq2i | |
19 | unidm | |
|
20 | 4 18 19 | 3eqtri | |
21 | 3 20 | sseqtrdi | |
22 | trclfvlb | |
|
23 | dmss | |
|
24 | 22 23 | syl | |
25 | 21 24 | eqssd | |