Metamath Proof Explorer


Definition df-wrecs

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 F , a relation R , and a base set A , this definition generates a function G = wrecs ( R , A , F ) that has property that, at any point x e. A , ( Gx ) = ( F` ( G |`Pred ( R , A , x ) ) ) . See wfr1 , wfr2 , and wfr3 . (Contributed by Scott Fenton, 7-Jun-2018) (Revised by BJ, 27-Oct-2024)

Ref Expression
Assertion df-wrecs wrecs ( 𝑅 , 𝐴 , 𝐹 ) = frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 𝑅
1 cA 𝐴
2 cF 𝐹
3 1 0 2 cwrecs wrecs ( 𝑅 , 𝐴 , 𝐹 )
4 c2nd 2nd
5 2 4 ccom ( 𝐹 ∘ 2nd )
6 1 0 5 cfrecs frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) )
7 3 6 wceq wrecs ( 𝑅 , 𝐴 , 𝐹 ) = frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) )