Theorem csbwrecsg

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

	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		csbuni	$$⊢⦋A/x⦌\bigcup \left\{f|\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}=\bigcup ⦋A/x⦌\left\{f|\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}$$
2		csbab	$$⊢⦋A/x⦌\left\{f|\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}=\left\{f|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}$$
3		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\leftrightarrow \exists z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)$$
4		sbc3an	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}fFnz\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)$$
5		sbcg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}fFnz\leftrightarrow fFnz\right)$$
6		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\subseteq D\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zPred\left(R,D,y\right)\subseteq z\right)$$
7		sbcssg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\subseteq D\leftrightarrow ⦋A/x⦌z\subseteq ⦋A/x⦌D\right)$$
8		csbconstg	$$⊢A\in V\to ⦋A/x⦌z=z$$
9	8	sseq1d	$$⊢A\in V\to \left(⦋A/x⦌z\subseteq ⦋A/x⦌D\leftrightarrow z\subseteq ⦋A/x⦌D\right)$$
10	7 9	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\subseteq D\leftrightarrow z\subseteq ⦋A/x⦌D\right)$$
11		sbcralg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zPred\left(R,D,y\right)\subseteq z\leftrightarrow \forall y\in z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}Pred\left(R,D,y\right)\subseteq z\right)$$
12		sbcssg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}Pred\left(R,D,y\right)\subseteq z\leftrightarrow ⦋A/x⦌Pred\left(R,D,y\right)\subseteq ⦋A/x⦌z\right)$$
13	8	sseq2d	$$⊢A\in V\to \left(⦋A/x⦌Pred\left(R,D,y\right)\subseteq ⦋A/x⦌z\leftrightarrow ⦋A/x⦌Pred\left(R,D,y\right)\subseteq z\right)$$
14		csbpredg	$$⊢A\in V\to ⦋A/x⦌Pred\left(R,D,y\right)=Pred\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌y\right)$$
15		csbconstg	$$⊢A\in V\to ⦋A/x⦌y=y$$
16		predeq3	$$⊢⦋A/x⦌y=y\to Pred\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌y\right)=Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)$$
17	15 16	syl	$$⊢A\in V\to Pred\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌y\right)=Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)$$
18	14 17	eqtrd	$$⊢A\in V\to ⦋A/x⦌Pred\left(R,D,y\right)=Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)$$
19	18	sseq1d	$$⊢A\in V\to \left(⦋A/x⦌Pred\left(R,D,y\right)\subseteq z\leftrightarrow Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)$$
20	12 13 19	3bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}Pred\left(R,D,y\right)\subseteq z\leftrightarrow Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)$$
21	20	ralbidv	$$⊢A\in V\to \left(\forall y\in z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}Pred\left(R,D,y\right)\subseteq z\leftrightarrow \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)$$
22	11 21	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zPred\left(R,D,y\right)\subseteq z\leftrightarrow \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)$$
23	10 22	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\subseteq D\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zPred\left(R,D,y\right)\subseteq z\right)\leftrightarrow \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\right)$$
24	6 23	syl5bb	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\leftrightarrow \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\right)$$
25		sbcralg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow \forall y\in z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}f\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)$$
26		sbceqg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}f\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow ⦋A/x⦌f\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)$$
27		csbconstg	$$⊢A\in V\to ⦋A/x⦌f\left(y\right)=f\left(y\right)$$
28		csbfv12	$$⊢⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)=⦋A/x⦌F\left(⦋A/x⦌\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)$$
29		csbres	$$⊢⦋A/x⦌\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)={⦋A/x⦌f\upharpoonright }_{⦋A/x⦌Pred\left(R,D,y\right)}$$
30		csbconstg	$$⊢A\in V\to ⦋A/x⦌f=f$$
31	30 18	reseq12d	$$⊢A\in V\to {⦋A/x⦌f\upharpoonright }_{⦋A/x⦌Pred\left(R,D,y\right)}={f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}$$
32	29 31	syl5eq	$$⊢A\in V\to ⦋A/x⦌\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)={f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}$$
33	32	fveq2d	$$⊢A\in V\to ⦋A/x⦌F\left(⦋A/x⦌\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)$$
34	28 33	syl5eq	$$⊢A\in V\to ⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)$$
35	27 34	eqeq12d	$$⊢A\in V\to \left(⦋A/x⦌f\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow f\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)$$
36	26 35	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}f\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow f\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)$$
37	36	ralbidv	$$⊢A\in V\to \left(\forall y\in z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}f\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)$$
38	25 37	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)$$
39	5 24 38	3anbi123d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}fFnz\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\leftrightarrow \left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right)$$
40	4 39	syl5bb	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\leftrightarrow \left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right)$$
41	40	exbidv	$$⊢A\in V\to \left(\exists z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\leftrightarrow \exists z\left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right)$$
42	3 41	syl5bb	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\leftrightarrow \exists z\left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right)$$
43	42	abbidv	$$⊢A\in V\to \left\{f|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}=\left\{f|\exists z\left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
44	2 43	syl5eq	$$⊢A\in V\to ⦋A/x⦌\left\{f|\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}=\left\{f|\exists z\left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
45	44	unieqd	$$⊢A\in V\to \bigcup ⦋A/x⦌\left\{f|\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}=\bigcup \left\{f|\exists z\left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
46	1 45	syl5eq	$$⊢A\in V\to ⦋A/x⦌\bigcup \left\{f|\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}=\bigcup \left\{f|\exists z\left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
47		df-wrecs	$$⊢\mathrm{wrecs}\left(R,D,F\right)=\bigcup \left\{f|\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}$$
48	47	csbeq2i	$$⊢⦋A/x⦌\mathrm{wrecs}\left(R,D,F\right)=⦋A/x⦌\bigcup \left\{f|\exists z\left(fFnz\wedge \left(z\subseteq D\wedge \forall y\in zPred\left(R,D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}$$
49		df-wrecs	$$⊢\mathrm{wrecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\right)=\bigcup \left\{f|\exists z\left(fFnz\wedge \left(z\subseteq ⦋A/x⦌D\wedge \forall y\in zPred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)\wedge \forall y\in zf\left(y\right)=⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
50	46 48 49	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)$$