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	$$⊢\mathrm{t*rec}=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crtrcl	$$class\mathrm{t*rec}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vn	$$setvarn$$
4		cn0	$$class{\mathbb{N}}_0$$
5	1	cv	$$setvarr$$
6		crelexp	$$class{\uparrow }_r$$
7	3	cv	$$setvarn$$
8	5 7 6	co	$$class\left(r{\uparrow }_{r}n\right)$$
9	3 4 8	ciun	$$class\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)$$
10	1 2 9	cmpt	$$class\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)$$
11	0 10	wceq	$$wff\mathrm{t*rec}=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)$$