Theorem wfrlem1OLD

Description: Lemma for well-ordered recursion. The final item we are interested in is the union of acceptable functions B . This lemma just changes bound variables for later use. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011)

	Ref	Expression
Hypothesis	wfrlem1OLD.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)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
Assertion	wfrlem1OLD	$$⊢B=\left\{g|\exists z\left(gFnz\wedge \left(z\subseteq A\wedge \forall w\in zPred\left(R,A,w\right)\subseteq z\right)\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		wfrlem1OLD.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)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
2		fneq1	$$⊢f=g\to \left(fFnx\leftrightarrow gFnx\right)$$
3		fveq1	$$⊢f=g\to f\left(y\right)=g\left(y\right)$$
4		reseq1	$$⊢f=g\to {f\upharpoonright }_{Pred\left(R,A,y\right)}={g\upharpoonright }_{Pred\left(R,A,y\right)}$$
5	4	fveq2d	$$⊢f=g\to F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)$$
6	3 5	eqeq12d	$$⊢f=g\to \left(f\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\leftrightarrow g\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)$$
7	6	ralbidv	$$⊢f=g\to \left(\forall y\in xf\left(y\right)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\leftrightarrow \forall y\in xg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)$$
8	2 7	3anbi13d	$$⊢f=g\to \left(\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)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\leftrightarrow \left(gFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right)$$
9	8	exbidv	$$⊢f=g\to \left(\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)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\leftrightarrow \exists x\left(gFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right)$$
10		fneq2	$$⊢x=z\to \left(gFnx\leftrightarrow gFnz\right)$$
11		sseq1	$$⊢x=z\to \left(x\subseteq A\leftrightarrow z\subseteq A\right)$$
12		sseq2	$$⊢x=z\to \left(Pred\left(R,A,y\right)\subseteq x\leftrightarrow Pred\left(R,A,y\right)\subseteq z\right)$$
13	12	raleqbi1dv	$$⊢x=z\to \left(\forall y\in xPred\left(R,A,y\right)\subseteq x\leftrightarrow \forall y\in zPred\left(R,A,y\right)\subseteq z\right)$$
14		predeq3	$$⊢y=w\to Pred\left(R,A,y\right)=Pred\left(R,A,w\right)$$
15	14	sseq1d	$$⊢y=w\to \left(Pred\left(R,A,y\right)\subseteq z\leftrightarrow Pred\left(R,A,w\right)\subseteq z\right)$$
16	15	cbvralvw	$$⊢\forall y\in zPred\left(R,A,y\right)\subseteq z\leftrightarrow \forall w\in zPred\left(R,A,w\right)\subseteq z$$
17	13 16	bitrdi	$$⊢x=z\to \left(\forall y\in xPred\left(R,A,y\right)\subseteq x\leftrightarrow \forall w\in zPred\left(R,A,w\right)\subseteq z\right)$$
18	11 17	anbi12d	$$⊢x=z\to \left(\left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\leftrightarrow \left(z\subseteq A\wedge \forall w\in zPred\left(R,A,w\right)\subseteq z\right)\right)$$
19		raleq	$$⊢x=z\to \left(\forall y\in xg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\leftrightarrow \forall y\in zg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)$$
20		fveq2	$$⊢y=w\to g\left(y\right)=g\left(w\right)$$
21	14	reseq2d	$$⊢y=w\to {g\upharpoonright }_{Pred\left(R,A,y\right)}={g\upharpoonright }_{Pred\left(R,A,w\right)}$$
22	21	fveq2d	$$⊢y=w\to F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)$$
23	20 22	eqeq12d	$$⊢y=w\to \left(g\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\leftrightarrow g\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)\right)$$
24	23	cbvralvw	$$⊢\forall y\in zg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\leftrightarrow \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)$$
25	19 24	bitrdi	$$⊢x=z\to \left(\forall y\in xg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\leftrightarrow \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)\right)$$
26	10 18 25	3anbi123d	$$⊢x=z\to \left(\left(gFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\leftrightarrow \left(gFnz\wedge \left(z\subseteq A\wedge \forall w\in zPred\left(R,A,w\right)\subseteq z\right)\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)\right)\right)$$
27	26	cbvexvw	$$⊢\exists x\left(gFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xg\left(y\right)=F\left({g\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\leftrightarrow \exists z\left(gFnz\wedge \left(z\subseteq A\wedge \forall w\in zPred\left(R,A,w\right)\subseteq z\right)\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)\right)$$
28	9 27	bitrdi	$$⊢f=g\to \left(\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)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\leftrightarrow \exists z\left(gFnz\wedge \left(z\subseteq A\wedge \forall w\in zPred\left(R,A,w\right)\subseteq z\right)\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)\right)\right)$$
29	28	cbvabv	$$⊢\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)=F\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}=\left\{g|\exists z\left(gFnz\wedge \left(z\subseteq A\wedge \forall w\in zPred\left(R,A,w\right)\subseteq z\right)\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)\right)\right\}$$
30	1 29	eqtri	$$⊢B=\left\{g|\exists z\left(gFnz\wedge \left(z\subseteq A\wedge \forall w\in zPred\left(R,A,w\right)\subseteq z\right)\wedge \forall w\in zg\left(w\right)=F\left({g\upharpoonright }_{Pred\left(R,A,w\right)}\right)\right)\right\}$$