Theorem bnj1444

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

Proof

Step	Hyp	Ref	Expression
1		bnj1444.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1444.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1444.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		bnj1444.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1444.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1444.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1444.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1444.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		bnj1444.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		bnj1444.10	$$⊢P=\bigcup H$$
11		bnj1444.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
12		bnj1444.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
13		bnj1444.13	$$⊢W=⟨z,{Q\upharpoonright }_{pred\left(z,A,R\right)}⟩$$
14		bnj1444.14	$$⊢E=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
15		bnj1444.15	$$⊢\chi \to PFntrCl\left(x,A,R\right)$$
16		bnj1444.16	$$⊢\chi \to QFn\left(\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
17		bnj1444.17	$$⊢\theta \leftrightarrow \left(\chi \wedge z\in E\right)$$
18		bnj1444.18	$$⊢\eta \leftrightarrow \left(\theta \wedge z\in \left\{x\right\}\right)$$
19		bnj1444.19	$$⊢\zeta \leftrightarrow \left(\theta \wedge z\in trCl\left(x,A,R\right)\right)$$
20		bnj1444.20	$$⊢\rho \leftrightarrow \left(\zeta \wedge f\in H\wedge z\in \mathrm{dom}f\right)$$
21		nfv	$$⊢Ⅎy\psi$$
22		nfv	$$⊢Ⅎyx\in D$$
23		nfra1	$$⊢Ⅎy\forall y\in D\neg yRx$$
24	21 22 23	nf3an	$$⊢Ⅎy\left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
25	7 24	nfxfr	$$⊢Ⅎy\chi$$
26		nfv	$$⊢Ⅎyz\in E$$
27	25 26	nfan	$$⊢Ⅎy\left(\chi \wedge z\in E\right)$$
28	17 27	nfxfr	$$⊢Ⅎy\theta$$
29		nfv	$$⊢Ⅎyz\in trCl\left(x,A,R\right)$$
30	28 29	nfan	$$⊢Ⅎy\left(\theta \wedge z\in trCl\left(x,A,R\right)\right)$$
31	19 30	nfxfr	$$⊢Ⅎy\zeta$$
32		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 |-
33	32	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 |-
34	9 33	nfcxfr	$$⊢\underset{\_}{Ⅎ}yH$$
35	34	nfcri	$$⊢Ⅎyf\in H$$
36		nfv	$$⊢Ⅎyz\in \mathrm{dom}f$$
37	31 35 36	nf3an	$$⊢Ⅎy\left(\zeta \wedge f\in H\wedge z\in \mathrm{dom}f\right)$$
38	20 37	nfxfr	$$⊢Ⅎy\rho$$
39	38	nf5ri	$$⊢\rho \to \forall y\rho$$