Theorem bnj1447

Description: Technical lemma for bnj60 . 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	bnj1447.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
	bnj1447.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
	bnj1447.3	$$⊢C=\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
	bnj1447.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
	bnj1447.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
	bnj1447.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
	bnj1447.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
	bnj1447.8	No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
	bnj1447.9	No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
	bnj1447.10	$$⊢P=\bigcup H$$
	bnj1447.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
	bnj1447.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
	bnj1447.13	$$⊢W=⟨z,{Q\upharpoonright }_{pred\left(z,A,R\right)}⟩$$
Assertion	bnj1447	$$⊢Q\left(z\right)=G\left(W\right)\to \forall yQ\left(z\right)=G\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj1447.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1447.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1447.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		bnj1447.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1447.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1447.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1447.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1447.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		bnj1447.9	Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
10		bnj1447.10	$$⊢P=\bigcup H$$
11		bnj1447.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
12		bnj1447.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
13		bnj1447.13	$$⊢W=⟨z,{Q\upharpoonright }_{pred\left(z,A,R\right)}⟩$$
14		nfre1	Could not format F/ y E. y e. _pred ( x , A , R ) ta' : No typesetting found for |- F/ y E. y e. _pred ( x , A , R ) ta' with typecode |-
15	14	nfab	Could not format F/_ y { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- F/_ y { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
16	9 15	nfcxfr	$$⊢\underset{\_}{Ⅎ}yH$$
17	16	nfuni	$$⊢\underset{\_}{Ⅎ}y\bigcup H$$
18	10 17	nfcxfr	$$⊢\underset{\_}{Ⅎ}yP$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}yx$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}yG$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}ypred\left(x,A,R\right)$$
22	18 21	nfres	$$⊢\underset{\_}{Ⅎ}y\left({P\upharpoonright }_{pred\left(x,A,R\right)}\right)$$
23	19 22	nfop	$$⊢\underset{\_}{Ⅎ}y⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
24	11 23	nfcxfr	$$⊢\underset{\_}{Ⅎ}yZ$$
25	20 24	nffv	$$⊢\underset{\_}{Ⅎ}yG\left(Z\right)$$
26	19 25	nfop	$$⊢\underset{\_}{Ⅎ}y⟨x,G\left(Z\right)⟩$$
27	26	nfsn	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,G\left(Z\right)⟩\right\}$$
28	18 27	nfun	$$⊢\underset{\_}{Ⅎ}y\left(P\cup \left\{⟨x,G\left(Z\right)⟩\right\}\right)$$
29	12 28	nfcxfr	$$⊢\underset{\_}{Ⅎ}yQ$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}yz$$
31	29 30	nffv	$$⊢\underset{\_}{Ⅎ}yQ\left(z\right)$$
32		nfcv	$$⊢\underset{\_}{Ⅎ}ypred\left(z,A,R\right)$$
33	29 32	nfres	$$⊢\underset{\_}{Ⅎ}y\left({Q\upharpoonright }_{pred\left(z,A,R\right)}\right)$$
34	30 33	nfop	$$⊢\underset{\_}{Ⅎ}y⟨z,{Q\upharpoonright }_{pred\left(z,A,R\right)}⟩$$
35	13 34	nfcxfr	$$⊢\underset{\_}{Ⅎ}yW$$
36	20 35	nffv	$$⊢\underset{\_}{Ⅎ}yG\left(W\right)$$
37	31 36	nfeq	$$⊢ℲyQ\left(z\right)=G\left(W\right)$$
38	37	nf5ri	$$⊢Q\left(z\right)=G\left(W\right)\to \forall yQ\left(z\right)=G\left(W\right)$$