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	$$⊢\mathrm{wrecs}\left(R,A,F\right)=\mathrm{frecs}\left(R,A,F\circ 2^{nd}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2		cF	$$classF$$
3	1 0 2	cwrecs	$$class\mathrm{wrecs}\left(R,A,F\right)$$
4		c2nd	$$class{2}^{nd}$$
5	2 4	ccom	$$class\left(F\circ 2^{nd}\right)$$
6	1 0 5	cfrecs	$$class\mathrm{frecs}\left(R,A,F\circ 2^{nd}\right)$$
7	3 6	wceq	$$wff\mathrm{wrecs}\left(R,A,F\right)=\mathrm{frecs}\left(R,A,F\circ 2^{nd}\right)$$