Description: Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | dfrtrcl4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfrtrcl3 | |
|
2 | df-n0 | |
|
3 | 2 | equncomi | |
4 | iuneq1 | |
|
5 | 3 4 | ax-mp | |
6 | iunxun | |
|
7 | 5 6 | eqtri | |
8 | c0ex | |
|
9 | oveq2 | |
|
10 | 8 9 | iunxsn | |
11 | 10 | a1i | |
12 | oveq1 | |
|
13 | 12 | iuneq2d | |
14 | dftrcl3 | |
|
15 | nnex | |
|
16 | ovex | |
|
17 | 15 16 | iunex | |
18 | 13 14 17 | fvmpt | |
19 | 18 | eqcomd | |
20 | 11 19 | uneq12d | |
21 | 7 20 | eqtrid | |
22 | 21 | mpteq2ia | |
23 | 1 22 | eqtri | |