Theorem bnj1467

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

Proof

Step	Hyp	Ref	Expression
1		bnj1467.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1467.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1467.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		bnj1467.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1467.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1467.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1467.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1467.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		bnj1467.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		bnj1467.10	$$⊢P=\bigcup H$$
11		bnj1467.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
12		bnj1467.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}dpred\left(x,A,R\right)$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}dy$$
15		nfre1	$$⊢Ⅎd\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)$$
16	15	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\}$$
17	3 16	nfcxfr	$$⊢\underset{\_}{Ⅎ}dC$$
18	17	nfcri	$$⊢Ⅎdf\in C$$
19		nfv	$$⊢Ⅎd\mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
20	18 19	nfan	$$⊢Ⅎd\left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
21	4 20	nfxfr	$$⊢Ⅎd\tau$$
22	14 21	nfsbcw	$$⊢Ⅎd\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\tau$$
23	8 22	nfxfr	Could not format F/ d ta' : No typesetting found for |- F/ d ta' with typecode |-
24	13 23	nfrex	Could not format F/ d E. y e. _pred ( x , A , R ) ta' : No typesetting found for |- F/ d E. y e. _pred ( x , A , R ) ta' with typecode |-
25	24	nfab	Could not format F/_ d { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- F/_ d { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
26	9 25	nfcxfr	$$⊢\underset{\_}{Ⅎ}dH$$
27	26	nfuni	$$⊢\underset{\_}{Ⅎ}d\bigcup H$$
28	10 27	nfcxfr	$$⊢\underset{\_}{Ⅎ}dP$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}dx$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}dG$$
31	28 13	nfres	$$⊢\underset{\_}{Ⅎ}d\left({P\upharpoonright }_{pred\left(x,A,R\right)}\right)$$
32	29 31	nfop	$$⊢\underset{\_}{Ⅎ}d⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
33	11 32	nfcxfr	$$⊢\underset{\_}{Ⅎ}dZ$$
34	30 33	nffv	$$⊢\underset{\_}{Ⅎ}dG\left(Z\right)$$
35	29 34	nfop	$$⊢\underset{\_}{Ⅎ}d⟨x,G\left(Z\right)⟩$$
36	35	nfsn	$$⊢\underset{\_}{Ⅎ}d\left\{⟨x,G\left(Z\right)⟩\right\}$$
37	28 36	nfun	$$⊢\underset{\_}{Ⅎ}d\left(P\cup \left\{⟨x,G\left(Z\right)⟩\right\}\right)$$
38	12 37	nfcxfr	$$⊢\underset{\_}{Ⅎ}dQ$$
39	38	nfcrii	$$⊢w\in Q\to \forall dw\in Q$$