Theorem bnj1519

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

Proof

Step	Hyp	Ref	Expression
1		bnj1519.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1519.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1519.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		bnj1519.4	$$⊢F=\bigcup C$$
5		nfre1	$$⊢Ⅎd\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)$$
6	5	nfab	$$⊢\underset{\_}{Ⅎ}d\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
7	3 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}dC$$
8	7	nfuni	$$⊢\underset{\_}{Ⅎ}d\bigcup C$$
9	4 8	nfcxfr	$$⊢\underset{\_}{Ⅎ}dF$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}dx$$
11	9 10	nffv	$$⊢\underset{\_}{Ⅎ}dF\left(x\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}dG$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}dpred\left(x,A,R\right)$$
14	9 13	nfres	$$⊢\underset{\_}{Ⅎ}d\left({F\upharpoonright }_{pred\left(x,A,R\right)}\right)$$
15	10 14	nfop	$$⊢\underset{\_}{Ⅎ}d⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
16	12 15	nffv	$$⊢\underset{\_}{Ⅎ}dG\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$
17	11 16	nfeq	$$⊢ℲdF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$
18	17	nf5ri	$$⊢F\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)\to \forall dF\left(x\right)=G\left(⟨x,{F\upharpoonright }_{pred\left(x,A,R\right)}⟩\right)$$