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 = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crtrcl	|- t*rec
1		vr	|- r
2		cvv	|- _V
3		vn	|- n
4		cn0	|- NN0
5	1	cv	|- r
6		crelexp	|- ^r
7	3	cv	|- n
8	5 7 6	co	|- ( r ^r n )
9	3 4 8	ciun	|- U_ n e. NN0 ( r ^r n )
10	1 2 9	cmpt	|- ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
11	0 10	wceq	|- t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )