Theorem tfrlem6

Description: Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994) (Revised by Mario Carneiro, 9-May-2015) Avoid ax-10 , ax-nul , ax-pr , ax-sep and ax-un . (Revised by Umit Teoman Dogan, 10-Jun-2026)

	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	tfrlem6	$$⊢\mathrm{Rel}\mathrm{recs}\left(F\right)$$

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		df-recs	$$⊢\mathrm{recs}\left(F\right)=\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},F\right)$$
3	2	wfrrel	$$⊢\mathrm{Rel}\mathrm{recs}\left(F\right)$$