Theorem frrrel

Description: Show without using the axiom of replacement that the well-founded recursion generator gives a relation. (Contributed by Scott Fenton, 18-Nov-2024)

	Ref	Expression
Hypothesis	frrrel.1	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
Assertion	frrrel	$$⊢\mathrm{Rel}F$$

Proof

Step	Hyp	Ref	Expression
1		frrrel.1	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
2		eqid	$$⊢\left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}=\left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
3	2 1	frrlem6	$$⊢\mathrm{Rel}F$$