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 13840
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 13839 . 2 class t*rec
2 vr . . 3 setvar 𝑟
3 cvv 3231 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 11330 . . . 4 class 0
62cv 1522 . . . . 5 class 𝑟
74cv 1522 . . . . 5 class 𝑛
8 crelexp 13804 . . . . 5 class 𝑟
96, 7, 8co 6690 . . . 4 class (𝑟𝑟𝑛)
104, 5, 9ciun 4552 . . 3 class 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)
112, 3, 10cmpt 4762 . 2 class (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
121, 11wceq 1523 1 wff t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
Colors of variables: wff setvar class
This definition is referenced by:  dfrtrclrec2  13841  rtrclreclem1  13842  rtrclreclem2  13843  rtrclreclem4  13845
  Copyright terms: Public domain W3C validator