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)

	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		reluni	$$⊢\mathrm{Rel}\bigcup A\leftrightarrow \forall g\in A\mathrm{Rel}g$$
3	1	tfrlem4	$$⊢g\in A\to \mathrm{Fun}g$$
4		funrel	$$⊢\mathrm{Fun}g\to \mathrm{Rel}g$$
5	3 4	syl	$$⊢g\in A\to \mathrm{Rel}g$$
6	2 5	mprgbir	$$⊢\mathrm{Rel}\bigcup A$$
7	1	recsfval	$$⊢\mathrm{recs}\left(F\right)=\bigcup A$$
8	7	releqi	$$⊢\mathrm{Rel}\mathrm{recs}\left(F\right)\leftrightarrow \mathrm{Rel}\bigcup A$$
9	6 8	mpbir	$$⊢\mathrm{Rel}\mathrm{recs}\left(F\right)$$