Definition df-frecs

Description: This is the definition for the well-founded recursion generator. Similar to df-wrecs and df-recs , it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a well-founded set-like relationship for its properties, not a well-ordered relationship. This proof requires either a partial order or the axiom of infinity. We develop the theorems twice, once with a partial order and once without. The second development occurs later in the database, after ax-inf has been introduced. (Contributed by Scott Fenton, 23-Dec-2021)

	Ref	Expression
Assertion	df-frecs	$$⊢\mathrm{frecs}\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)=yF\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	cfrecs	$$class\mathrm{frecs}\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	11 17 2	co	$$class\left(yF\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)$$
19	16 18	wceq	$$wfff\left(y\right)=yF\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
20	19 10 7	wral	$$wff\forall y\in xf\left(y\right)=yF\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)=yF\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)=yF\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)=yF\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)=yF\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
25	3 24	wceq	$$wff\mathrm{frecs}\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)=yF\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$