Theorem csbfrecsg

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

	Ref	Expression
Assertion	csbfrecsg	$$⊢A\in V\to ⦋A/x⦌\mathrm{frecs}\left(R,D,F\right)=\mathrm{frecs}\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)=yF\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)=yF\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)=yF\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)=yF\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)=yF\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)=yF\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)=yF\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)=yF\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		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)$$
14		csbconstg	$$⊢A\in V\to ⦋A/x⦌y=y$$
15		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)$$
16	14 15	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)$$
17	13 16	eqtrd	$$⊢A\in V\to ⦋A/x⦌Pred\left(R,D,y\right)=Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)$$
18	17 8	sseq12d	$$⊢A\in V\to \left(⦋A/x⦌Pred\left(R,D,y\right)\subseteq ⦋A/x⦌z\leftrightarrow Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)\subseteq z\right)$$
19	12 18	bitrd	$$⊢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)$$
20	19	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)$$
21	11 20	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)$$
22	10 21	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)$$
23	6 22	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)$$
24		sbcralg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zf\left(y\right)=yF\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)=yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)$$
25		sbceqg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}f\left(y\right)=yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow ⦋A/x⦌f\left(y\right)=⦋A/x⦌\left(yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right)$$
26		csbconstg	$$⊢A\in V\to ⦋A/x⦌f\left(y\right)=f\left(y\right)$$
27		csbov123	$$⊢⦋A/x⦌\left(yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)=⦋A/x⦌y⦋A/x⦌F⦋A/x⦌\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)$$
28		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)}$$
29		csbconstg	$$⊢A\in V\to ⦋A/x⦌f=f$$
30	29 17	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)}$$
31	28 30	eqtrid	$$⊢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)}$$
32	14 31	oveq12d	$$⊢A\in V\to ⦋A/x⦌y⦋A/x⦌F⦋A/x⦌\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)$$
33	27 32	eqtrid	$$⊢A\in V\to ⦋A/x⦌\left(yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)$$
34	26 33	eqeq12d	$$⊢A\in V\to \left(⦋A/x⦌f\left(y\right)=⦋A/x⦌\left(yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\leftrightarrow f\left(y\right)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)$$
35	25 34	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}f\left(y\right)=yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow f\left(y\right)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)$$
36	35	ralbidv	$$⊢A\in V\to \left(\forall y\in z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}f\left(y\right)=yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow \forall y\in zf\left(y\right)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)$$
37	24 36	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in zf\left(y\right)=yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\leftrightarrow \forall y\in zf\left(y\right)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)$$
38	5 23 37	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)=yF\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right)$$
39	4 38	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)=yF\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right)$$
40	39	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)=yF\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right)$$
41	3 40	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)=yF\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right)$$
42	41	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)=yF\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
43	2 42	eqtrid	$$⊢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)=yF\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
44	43	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)=yF\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
45	1 44	eqtrid	$$⊢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)=yF\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
46		df-frecs	$$⊢\mathrm{frecs}\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)=yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}$$
47	46	csbeq2i	$$⊢⦋A/x⦌\mathrm{frecs}\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)=yF\left({f\upharpoonright }_{Pred\left(R,D,y\right)}\right)\right)\right\}$$
48		df-frecs	$$⊢\mathrm{frecs}\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)=y⦋A/x⦌F\left({f\upharpoonright }_{Pred\left(⦋A/x⦌R,⦋A/x⦌D,y\right)}\right)\right)\right\}$$
49	45 47 48	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\mathrm{frecs}\left(R,D,F\right)=\mathrm{frecs}\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌F\right)$$