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 14866
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 14865 . 2 class t*rec
2 vr . . 3 setvar 𝑟
3 cvv 3441 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 cn0 12334 . . . 4 class 0
62cv 1539 . . . . 5 class 𝑟
74cv 1539 . . . . 5 class 𝑛
8 crelexp 14829 . . . . 5 class 𝑟
96, 7, 8co 7337 . . . 4 class (𝑟𝑟𝑛)
104, 5, 9ciun 4941 . . 3 class 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)
112, 3, 10cmpt 5175 . 2 class (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
121, 11wceq 1540 1 wff t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
Colors of variables: wff setvar class
This definition is referenced by:  rtrclreclem1  14867  dfrtrclrec2  14868  rtrclreclem2  14869  rtrclreclem4  14871
  Copyright terms: Public domain W3C validator