Theorem frrlem5

Description: Lemma for well-founded recursion. State the well-founded recursion generator in terms of the acceptable functions. (Contributed by Scott Fenton, 27-Aug-2022)

	Ref	Expression
Hypotheses	frrlem5.1	$$⊢B=\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)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
	frrlem5.2	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
Assertion	frrlem5	$$⊢F=\bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		frrlem5.1	$$⊢B=\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)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
2		frrlem5.2	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
3		df-frecs	$$⊢\mathrm{frecs}\left(R,A,G\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)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
4	1	unieqi	$$⊢\bigcup B=\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)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
5	3 2 4	3eqtr4i	$$⊢F=\bigcup B$$