Theorem bnj1520

Description: Technical lemma for bnj1500 . 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	bnj1520.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
	bnj1520.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
	bnj1520.3	$$⊢C=\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
	bnj1520.4	$$⊢F=\bigcup C$$
Assertion	bnj1520	$$⊢F\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)\to \forall fF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj1520.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1520.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1520.3	$$⊢C=\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
4		bnj1520.4	$$⊢F=\bigcup C$$
5	3	bnj1317	$$⊢w\in C\to \forall fw\in C$$
6	5	nfcii	$$⊢\underset{\_}{Ⅎ}fC$$
7	6	nfuni	$$⊢\underset{\_}{Ⅎ}f\bigcup C$$
8	4 7	nfcxfr	$$⊢\underset{\_}{Ⅎ}fF$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}fx$$
10	8 9	nffv	$$⊢\underset{\_}{Ⅎ}fF\left(x\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}fG$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}fpred\left(x,A,R\right)$$
13	8 12	nfres	$$⊢\underset{\_}{Ⅎ}f\left({F\upharpoonright }_{pred\left(x,A,R\right)}\right)$$
14	9 13	nfop	$$⊢\underset{\_}{Ⅎ}f⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
15	11 14	nffv	$$⊢\underset{\_}{Ⅎ}fG\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$
16	10 15	nfeq	$$⊢ℲfF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$
17	16	nf5ri	$$⊢F\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)\to \forall fF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$