Theorem csbwrecsg

Description: Move class substitution in and out of the well-founded recursive function generator. (Contributed by ML, 25-Oct-2020) (Revised by Scott Fenton, 18-Nov-2024)

	Ref	Expression
Assertion	csbwrecsg	$$⊢A\in V\to ⦋A/x⦌\mathrm{wrecs}\left(R,D,F\right)=\mathrm{wrecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbfrecsg	$$⊢A\in V\to ⦋A/x⦌\mathrm{frecs}\left(R,D,F\circ 2^{nd}\right)=\mathrm{frecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌\left(F\circ 2^{nd}\right)\right)$$
2		eqid	$$⊢⦋A/x⦌R=⦋A/x⦌R$$
3		eqid	$$⊢⦋A/x⦌D=⦋A/x⦌D$$
4		csbcog	$$⊢A\in V\to ⦋A/x⦌\left(F\circ 2^{nd}\right)=⦋A/x⦌F\circ ⦋A/x⦌2^{nd}$$
5		csbconstg	$$⊢A\in V\to ⦋A/x⦌2^{nd}=2^{nd}$$
6	5	coeq2d	$$⊢A\in V\to ⦋A/x⦌F\circ ⦋A/x⦌2^{nd}=⦋A/x⦌F\circ 2^{nd}$$
7	4 6	eqtrd	$$⊢A\in V\to ⦋A/x⦌\left(F\circ 2^{nd}\right)=⦋A/x⦌F\circ 2^{nd}$$
8		frecseq123	$$⊢\left(⦋A/x⦌R=⦋A/x⦌R\wedge ⦋A/x⦌D=⦋A/x⦌D\wedge ⦋A/x⦌\left(F\circ 2^{nd}\right)=⦋A/x⦌F\circ 2^{nd}\right)\to \mathrm{frecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌\left(F\circ 2^{nd}\right)\right)=\mathrm{frecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\circ 2^{nd}\right)$$
9	2 3 7 8	mp3an12i	$$⊢A\in V\to \mathrm{frecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌\left(F\circ 2^{nd}\right)\right)=\mathrm{frecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\circ 2^{nd}\right)$$
10	1 9	eqtrd	$$⊢A\in V\to ⦋A/x⦌\mathrm{frecs}\left(R,D,F\circ 2^{nd}\right)=\mathrm{frecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\circ 2^{nd}\right)$$
11		df-wrecs	$$⊢\mathrm{wrecs}\left(R,D,F\right)=\mathrm{frecs}\left(R,D,F\circ 2^{nd}\right)$$
12	11	csbeq2i	$$⊢⦋A/x⦌\mathrm{wrecs}\left(R,D,F\right)=⦋A/x⦌\mathrm{frecs}\left(R,D,F\circ 2^{nd}\right)$$
13		df-wrecs	$$⊢\mathrm{wrecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\right)=\mathrm{frecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\circ 2^{nd}\right)$$
14	10 12 13	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\mathrm{wrecs}\left(R,D,F\right)=\mathrm{wrecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\right)$$