Theorem bnj1529

Description: Technical lemma for bnj1522 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1529.1	$$⊢\chi \to \forall x\in AF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$
	bnj1529.2	$$⊢w\in F\to \forall xw\in F$$
Assertion	bnj1529	$$⊢\chi \to \forall y\in AF\left(y\right)=G\left(⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj1529.1	$$⊢\chi \to \forall x\in AF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$
2		bnj1529.2	$$⊢w\in F\to \forall xw\in F$$
3		nfv	$$⊢ℲyF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$
4	2	nfcii	$$⊢\underset{\_}{Ⅎ}xF$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
6	4 5	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xG$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xpred\left(y,A,R\right)$$
9	4 8	nfres	$$⊢\underset{\_}{Ⅎ}x\left({F\upharpoonright }_{pred\left(y,A,R\right)}\right)$$
10	5 9	nfop	$$⊢\underset{\_}{Ⅎ}x⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩$$
11	7 10	nffv	$$⊢\underset{\_}{Ⅎ}xG\left(⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩\right)$$
12	6 11	nfeq	$$⊢ℲxF\left(y\right)=G\left(⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩\right)$$
13		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
14		id	$$⊢x=y\to x=y$$
15		bnj602	$$⊢x=y\to pred\left(x,A,R\right)=pred\left(y,A,R\right)$$
16	15	reseq2d	$$⊢x=y\to {F\upharpoonright }_{pred\left(x,A,R\right)}={F\upharpoonright }_{pred\left(y,A,R\right)}$$
17	14 16	opeq12d	$$⊢x=y\to ⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩=⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩$$
18	17	fveq2d	$$⊢x=y\to G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)=G\left(⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩\right)$$
19	13 18	eqeq12d	$$⊢x=y\to \left(F\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)\leftrightarrow F\left(y\right)=G\left(⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩\right)\right)$$
20	3 12 19	cbvralw	$$⊢\forall x\in AF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)\leftrightarrow \forall y\in AF\left(y\right)=G\left(⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩\right)$$
21	1 20	sylib	$$⊢\chi \to \forall y\in AF\left(y\right)=G\left(⟨y,{F\upharpoonright }_{pred\left(y,A,R\right)}⟩\right)$$