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

Definition df-wrecs 8137
Description: Define the well-ordered recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function 𝐹, a relation 𝑅, and a base set 𝐴, this definition generates a function 𝐺 = wrecs(𝑅, 𝐴, 𝐹) that has property that, at any point 𝑥𝐴, (𝐺𝑥) = (𝐹‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑥))). See wfr1 8175, wfr2 8176, and wfr3 8177. (Contributed by Scott Fenton, 7-Jun-2018.) (Revised by BJ, 27-Oct-2024.)
Assertion
Ref Expression
df-wrecs wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd ))

Detailed syntax breakdown of Definition df-wrecs
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
3 cF . . 3 class 𝐹
41, 2, 3cwrecs 8136 . 2 class wrecs(𝑅, 𝐴, 𝐹)
5 c2nd 7839 . . . 4 class 2nd
63, 5ccom 5594 . . 3 class (𝐹 ∘ 2nd )
71, 2, 6cfrecs 8105 . 2 class frecs(𝑅, 𝐴, (𝐹 ∘ 2nd ))
84, 7wceq 1539 1 wff wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd ))
Colors of variables: wff setvar class
This definition is referenced by:  dfwrecsOLD  8138  wrecseq123  8139  nfwrecs  8141  csbwrecsg  8146  wfrrel  8169  wfrdmss  8170  wfrdmcl  8171  wfrfun  8172  wfrresex  8173  wfr2a  8174  wfr1  8175  dfrecs3  8212
  Copyright terms: Public domain W3C validator