Description: The reflexive, transitive closure of a relation constructed as the union of all finite exponentiations. (Contributed by Drahflow, 12-Nov-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-rtrclrec | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | crtrcl | |
|
1 | vr | |
|
2 | cvv | |
|
3 | vn | |
|
4 | cn0 | |
|
5 | 1 | cv | |
6 | crelexp | |
|
7 | 3 | cv | |
8 | 5 7 6 | co | |
9 | 3 4 8 | ciun | |
10 | 1 2 9 | cmpt | |
11 | 0 10 | wceq | |