Theorem recsfval

Description: Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypothesis	tfrlem.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	recsfval	$$⊢\mathrm{recs}\left(F\right)=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		tfrlem.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		dfrecs3	$$⊢\mathrm{recs}\left(F\right)=\bigcup \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\}$$
3	1	unieqi	$$⊢\bigcup A=\bigcup \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\}$$
4	2 3	eqtr4i	$$⊢\mathrm{recs}\left(F\right)=\bigcup A$$