Definition df-wrecs

Description: Here we define the well-founded recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function F , a relationship 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) (New usage is discouraged.)

	Ref	Expression
Assertion	df-wrecs	$$⊢\mathrm{wrecs}\left(R,A,F\right)=\bigcup \left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\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		vf	$$setvarf$$
5		vx	$$setvarx$$
6	4	cv	$$setvarf$$
7	5	cv	$$setvarx$$
8	6 7	wfn	$$wfffFnx$$
9	7 1	wss	$$wffx\subseteq A$$
10		vy	$$setvary$$
11	10	cv	$$setvary$$
12	1 0 11	cpred	$$classPred\left(R,A,y\right)$$
13	12 7	wss	$$wffPred\left(R,A,y\right)\subseteq x$$
14	13 10 7	wral	$$wff\forall y\in xPred\left(R,A,y\right)\subseteq x$$
15	9 14	wa	$$wff\left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)$$
16	11 6	cfv	$$classf\left(y\right)$$
17	6 12	cres	$$class\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
18	17 2	cfv	$$classF\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
19	16 18	wceq	$$wfff\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
20	19 10 7	wral	$$wff\forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
21	8 15 20	w3a	$$wff\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)$$
22	21 5	wex	$$wff\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)$$
23	22 4	cab	$$class\left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
24	23	cuni	$$class\bigcup \left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
25	3 24	wceq	$$wff\mathrm{wrecs}\left(R,A,F\right)=\bigcup \left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$