Theorem dfwrecsOLD

Description: Obsolete definition of the well-ordered recursive function generator as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 7-Jun-2018)

	Ref	Expression
Assertion	dfwrecsOLD	$$⊢\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\}$$

Proof

Step	Hyp	Ref	Expression
1		df-wrecs	$$⊢\mathrm{wrecs}\left(R,A,F\right)=\mathrm{frecs}\left(R,A,F\circ 2^{nd}\right)$$
2		df-frecs	$$⊢\mathrm{frecs}\left(R,A,F\circ 2^{nd}\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)=y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	3	a1i	$$⊢\top \to y\in \mathrm{V}$$
5		vex	$$⊢f\in \mathrm{V}$$
6	5	resex	$$⊢{f\upharpoonright }_{Pred\left(R,A,y\right)}\in \mathrm{V}$$
7	6	a1i	$$⊢\top \to {f\upharpoonright }_{Pred\left(R,A,y\right)}\in \mathrm{V}$$
8	4 7	opco2	$$⊢\top \to y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
9	8	mptru	$$⊢y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
10	9	eqeq2i	$$⊢f\left(y\right)=y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\leftrightarrow f\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
11	10	ralbii	$$⊢\forall y\in xf\left(y\right)=y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\leftrightarrow \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
12	11	3anbi3i	$$⊢\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)=y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\leftrightarrow \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)$$
13	12	exbii	$$⊢\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)=y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\leftrightarrow \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)$$
14	13	abbii	$$⊢\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)=y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}=\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\}$$
15	14	unieqi	$$⊢\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)=y\left(F\circ 2^{nd}\right)\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\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\}$$
16	1 2 15	3eqtri	$$⊢\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\}$$