Theorem frrlem6

Description: Lemma for well-founded recursion. The well-founded recursion generator is a relationship. (Contributed by Scott Fenton, 27-Aug-2022)

	Ref	Expression
Hypotheses	frrlem5.1	$$⊢B=\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\}$$
	frrlem5.2	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
Assertion	frrlem6	$$⊢\mathrm{Rel}F$$

Proof

Step	Hyp	Ref	Expression
1		frrlem5.1	$$⊢B=\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\}$$
2		frrlem5.2	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
3	1 2	frrlem5	$$⊢F=\bigcup B$$
4	3	releqi	$$⊢\mathrm{Rel}F\leftrightarrow \mathrm{Rel}\bigcup B$$
5		reluni	$$⊢\mathrm{Rel}\bigcup B\leftrightarrow \forall g\in B\mathrm{Rel}g$$
6	4 5	bitri	$$⊢\mathrm{Rel}F\leftrightarrow \forall g\in B\mathrm{Rel}g$$
7	1	frrlem2	$$⊢g\in B\to \mathrm{Fun}g$$
8		funrel	$$⊢\mathrm{Fun}g\to \mathrm{Rel}g$$
9	7 8	syl	$$⊢g\in B\to \mathrm{Rel}g$$
10	6 9	mprgbir	$$⊢\mathrm{Rel}F$$