| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-wrecs | Structured version Visualization version GIF version | ||
| 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 8375, wfr2 8376, and wfr3 8377. (Contributed by Scott Fenton, 7-Jun-2018.) (Revised by BJ, 27-Oct-2024.) |
| Ref | Expression |
|---|---|
| df-wrecs | ⊢ wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd )) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cR | . . 3 class 𝑅 | |
| 3 | cF | . . 3 class 𝐹 | |
| 4 | 1, 2, 3 | cwrecs 8336 | . 2 class wrecs(𝑅, 𝐴, 𝐹) |
| 5 | c2nd 8013 | . . . 4 class 2nd | |
| 6 | 3, 5 | ccom 5689 | . . 3 class (𝐹 ∘ 2nd ) |
| 7 | 1, 2, 6 | cfrecs 8305 | . 2 class frecs(𝑅, 𝐴, (𝐹 ∘ 2nd )) |
| 8 | 4, 7 | wceq 1540 | 1 wff wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd )) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfwrecsOLD 8338 wrecseq123 8339 nfwrecs 8341 csbwrecsg 8346 wfrrel 8369 wfrdmss 8370 wfrdmcl 8371 wfrfun 8372 wfrresex 8373 wfr2a 8374 wfr1 8375 dfrecs3 8412 |
| Copyright terms: Public domain | W3C validator |