Theorem wfr2aOLD

Description: Obsolete version of wfr2a as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 30-Jul-2020)

	Ref	Expression
Hypotheses	wfr2aOLD.1	$$⊢R\mathrm{We}A$$
	wfr2aOLD.2	$$⊢R\mathrm{Se}A$$
	wfr2aOLD.3	$$⊢F=\mathrm{wrecs}\left(R,A,G\right)$$
Assertion	wfr2aOLD	$$⊢X\in \mathrm{dom}F\to F\left(X\right)=G\left({F\upharpoonright }_{Pred\left(R,A,X\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		wfr2aOLD.1	$$⊢R\mathrm{We}A$$
2		wfr2aOLD.2	$$⊢R\mathrm{Se}A$$
3		wfr2aOLD.3	$$⊢F=\mathrm{wrecs}\left(R,A,G\right)$$
4		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
5		predeq3	$$⊢x=X\to Pred\left(R,A,x\right)=Pred\left(R,A,X\right)$$
6	5	reseq2d	$$⊢x=X\to {F\upharpoonright }_{Pred\left(R,A,x\right)}={F\upharpoonright }_{Pred\left(R,A,X\right)}$$
7	6	fveq2d	$$⊢x=X\to G\left({F\upharpoonright }_{Pred\left(R,A,x\right)}\right)=G\left({F\upharpoonright }_{Pred\left(R,A,X\right)}\right)$$
8	4 7	eqeq12d	$$⊢x=X\to \left(F\left(x\right)=G\left({F\upharpoonright }_{Pred\left(R,A,x\right)}\right)\leftrightarrow F\left(X\right)=G\left({F\upharpoonright }_{Pred\left(R,A,X\right)}\right)\right)$$
9	1 2 3	wfrlem12OLD	$$⊢x\in \mathrm{dom}F\to F\left(x\right)=G\left({F\upharpoonright }_{Pred\left(R,A,x\right)}\right)$$
10	8 9	vtoclga	$$⊢X\in \mathrm{dom}F\to F\left(X\right)=G\left({F\upharpoonright }_{Pred\left(R,A,X\right)}\right)$$