Theorem nfrdg

Description: Bound-variable hypothesis builder for the recursive definition generator. (Contributed by NM, 14-Sep-2003) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Hypotheses	nfrdg.1	$$⊢\underset{\_}{Ⅎ}xF$$
	nfrdg.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfrdg	$$⊢\underset{\_}{Ⅎ}x\mathrm{rec}\left(F,A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfrdg.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nfrdg.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-rdg	$$⊢\mathrm{rec}\left(F,A\right)=\mathrm{recs}\left(\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{V}$$
5		nfv	$$⊢Ⅎxg=\varnothing$$
6		nfv	$$⊢Ⅎx\mathrm{Lim}\mathrm{dom}g$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}x\bigcup \mathrm{ran}g$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xg\left(\bigcup \mathrm{dom}g\right)$$
9	1 8	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(g\left(\bigcup \mathrm{dom}g\right)\right)$$
10	6 7 9	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)$$
11	5 2 10	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(g=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)$$
12	4 11	nfmpt	$$⊢\underset{\_}{Ⅎ}x\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)$$
13	12	nfrecs	$$⊢\underset{\_}{Ⅎ}x\mathrm{recs}\left(\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\right)$$
14	3 13	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\mathrm{rec}\left(F,A\right)$$