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

Definition df-rtrclrec 13644
 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 13643 . 2 class t*rec
2 vr . . 3 setvar 𝑟
3 cvv 3173 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11169 . . . 4 class 0
62cv 1474 . . . . 5 class 𝑟
74cv 1474 . . . . 5 class 𝑛
8 crelexp 13608 . . . . 5 class 𝑟
96, 7, 8co 6549 . . . 4 class (𝑟𝑟𝑛)
104, 5, 9ciun 4455 . . 3 class 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)
112, 3, 10cmpt 4643 . 2 class (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
121, 11wceq 1475 1 wff t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
 Colors of variables: wff setvar class This definition is referenced by:  dfrtrclrec2  13645  rtrclreclem1  13646  rtrclreclem2  13647  rtrclreclem4  13649
 Copyright terms: Public domain W3C validator