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 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crtrcl	⊢ t*rec
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vn	⊢ 𝑛
4		cn0	⊢ ℕ0
5	1	cv	⊢ 𝑟
6		crelexp	⊢ ↑𝑟
7	3	cv	⊢ 𝑛
8	5 7 6	co	⊢ ( 𝑟 ↑𝑟 𝑛 )
9	3 4 8	ciun	⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 )
10	1 2 9	cmpt	⊢ ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
11	0 10	wceq	⊢ t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )