Theorem nffrecs

Description: Bound-variable hypothesis builder for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021)

	Ref	Expression
Hypotheses	nffrecs.1	$$⊢\underset{\_}{Ⅎ}xR$$
	nffrecs.2	$$⊢\underset{\_}{Ⅎ}xA$$
	nffrecs.3	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	nffrecs	$$⊢\underset{\_}{Ⅎ}x\mathrm{frecs}\left(R,A,F\right)$$

Proof

Step	Hyp	Ref	Expression
1		nffrecs.1	$$⊢\underset{\_}{Ⅎ}xR$$
2		nffrecs.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nffrecs.3	$$⊢\underset{\_}{Ⅎ}xF$$
4		df-frecs	$$⊢\mathrm{frecs}\left(R,A,F\right)=\bigcup \left\{f|\exists y\left(fFny\wedge \left(y\subseteq A\wedge \forall z\in yPred\left(R,A,z\right)\subseteq y\right)\wedge \forall z\in yf\left(z\right)=zF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)\right)\right\}$$
5		nfv	$$⊢ℲxfFny$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
7	6 2	nfss	$$⊢Ⅎxy\subseteq A$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
9	1 2 8	nfpred	$$⊢\underset{\_}{Ⅎ}xPred\left(R,A,z\right)$$
10	9 6	nfss	$$⊢ℲxPred\left(R,A,z\right)\subseteq y$$
11	6 10	nfralw	$$⊢Ⅎx\forall z\in yPred\left(R,A,z\right)\subseteq y$$
12	7 11	nfan	$$⊢Ⅎx\left(y\subseteq A\wedge \forall z\in yPred\left(R,A,z\right)\subseteq y\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}xf$$
14	13 9	nfres	$$⊢\underset{\_}{Ⅎ}x\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)$$
15	8 3 14	nfov	$$⊢\underset{\_}{Ⅎ}x\left(zF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)\right)$$
16	15	nfeq2	$$⊢Ⅎxf\left(z\right)=zF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)$$
17	6 16	nfralw	$$⊢Ⅎx\forall z\in yf\left(z\right)=zF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)$$
18	5 12 17	nf3an	$$⊢Ⅎx\left(fFny\wedge \left(y\subseteq A\wedge \forall z\in yPred\left(R,A,z\right)\subseteq y\right)\wedge \forall z\in yf\left(z\right)=zF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)\right)$$
19	18	nfex	$$⊢Ⅎx\exists y\left(fFny\wedge \left(y\subseteq A\wedge \forall z\in yPred\left(R,A,z\right)\subseteq y\right)\wedge \forall z\in yf\left(z\right)=zF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)\right)$$
20	19	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{f|\exists y\left(fFny\wedge \left(y\subseteq A\wedge \forall z\in yPred\left(R,A,z\right)\subseteq y\right)\wedge \forall z\in yf\left(z\right)=zF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)\right)\right\}$$
21	20	nfuni	$$⊢\underset{\_}{Ⅎ}x\bigcup \left\{f|\exists y\left(fFny\wedge \left(y\subseteq A\wedge \forall z\in yPred\left(R,A,z\right)\subseteq y\right)\wedge \forall z\in yf\left(z\right)=zF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)\right)\right\}$$
22	4 21	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\mathrm{frecs}\left(R,A,F\right)$$