Theorem dfwrecs2

Description: TODO: Replace df-wrecs with this definition, and shorten theorems using wrecs with it. (Contributed by BJ, 27-Oct-2024)

	Ref	Expression
Assertion	dfwrecs2	$$⊢\mathrm{wrecs}\left(R,A,F\right)=\mathrm{frecs}\left(R,A,F\circ 2^{nd}\right)$$

Proof

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