Metamath Proof Explorer


Definition df-rtrclrec

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 t*rec=rVn0rrn

Detailed syntax breakdown

Step Hyp Ref Expression
0 crtrcl classt*rec
1 vr setvarr
2 cvv classV
3 vn setvarn
4 cn0 class0
5 1 cv setvarr
6 crelexp classr
7 3 cv setvarn
8 5 7 6 co classrrn
9 3 4 8 ciun classn0rrn
10 1 2 9 cmpt classrVn0rrn
11 0 10 wceq wfft*rec=rVn0rrn