Theorem wfrrel

Description: The well-ordered recursion generator generates a relationship. (Contributed by Scott Fenton, 8-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		wfrlem6.1	$$⊢F=\mathrm{wrecs}\left(R,A,G\right)$$
2		reluni	$$⊢\mathrm{Rel}\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}\leftrightarrow \forall g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}\mathrm{Rel}g$$
3		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)=G\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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
4	3	wfrlem2	$$⊢g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}\to \mathrm{Fun}g$$
5		funrel	$$⊢\mathrm{Fun}g\to \mathrm{Rel}g$$
6	4 5	syl	$$⊢g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}\to \mathrm{Rel}g$$
7	2 6	mprgbir	$$⊢\mathrm{Rel}\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
8		df-wrecs	$$⊢\mathrm{wrecs}\left(R,A,G\right)=\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
9	1 8	eqtri	$$⊢F=\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
10	9	releqi	$$⊢\mathrm{Rel}F\leftrightarrow \mathrm{Rel}\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
11	7 10	mpbir	$$⊢\mathrm{Rel}F$$