MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rtrclrec Structured version   Visualization version   GIF version

Definition df-rtrclrec 13590
Description: The reflexive, transitive closure of a relation constructed as the union of all finite exponentiations. (Contributed by Drahflow, 12-Nov-2015.)
Assertion
Ref Expression
df-rtrclrec t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
Distinct variable group:   𝑛,𝑟

Detailed syntax breakdown of Definition df-rtrclrec
StepHypRef Expression
1 crtrcl 13589 . 2 class t*rec
2 vr . . 3 setvar 𝑟
3 cvv 3172 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11139 . . . 4 class 0
62cv 1473 . . . . 5 class 𝑟
74cv 1473 . . . . 5 class 𝑛
8 crelexp 13554 . . . . 5 class 𝑟
96, 7, 8co 6527 . . . 4 class (𝑟𝑟𝑛)
104, 5, 9ciun 4449 . . 3 class 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)
112, 3, 10cmpt 4637 . 2 class (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
121, 11wceq 1474 1 wff t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
Colors of variables: wff setvar class
This definition is referenced by:  dfrtrclrec2  13591  rtrclreclem1  13592  rtrclreclem2  13593  rtrclreclem4  13595
  Copyright terms: Public domain W3C validator