Theorem tfrlem3

Description: Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995)

	Ref	Expression
Hypothesis	tfrlem3.1	$$⊢A=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_y\right)\right)\right\}$$
Assertion	tfrlem3	$$⊢A=\left\{g|\exists z\in \mathrm{On}\left(gFnz\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_w\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		tfrlem3.1	$$⊢A=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_y\right)\right)\right\}$$
2		vex	$$⊢g\in \mathrm{V}$$
3	1 2	tfrlem3a	$$⊢g\in A\leftrightarrow \exists z\in \mathrm{On}\left(gFnz\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_w\right)\right)$$
4	3	eqabi	$$⊢A=\left\{g|\exists z\in \mathrm{On}\left(gFnz\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_w\right)\right)\right\}$$