Theorem nfwrecs

Description: Bound-variable hypothesis builder for the well-founded recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		nfwrecs.1	$$⊢\underset{\_}{Ⅎ}xR$$
2		nfwrecs.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nfwrecs.3	$$⊢\underset{\_}{Ⅎ}xF$$
4		df-wrecs	$$⊢\mathrm{wrecs}\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)=F\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	3 14	nffv	$$⊢\underset{\_}{Ⅎ}xF\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)$$
16	15	nfeq2	$$⊢Ⅎxf\left(z\right)=F\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)$$
17	6 16	nfralw	$$⊢Ⅎx\forall z\in yf\left(z\right)=F\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)=F\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)=F\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)=F\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)=F\left({f\upharpoonright }_{Pred\left(R,A,z\right)}\right)\right)\right\}$$
22	4 21	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\mathrm{wrecs}\left(R,A,F\right)$$