Theorem bnj1442

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

Proof

Step	Hyp	Ref	Expression
1		bnj1442.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1442.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1442.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		bnj1442.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1442.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1442.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1442.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1442.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		bnj1442.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		bnj1442.10	$$⊢P=\bigcup H$$
11		bnj1442.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
12		bnj1442.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
13		bnj1442.13	$$⊢W=⟨z,{Q\upharpoonright }_{pred\left(z,A,R\right)}⟩$$
14		bnj1442.14	$$⊢E=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
15		bnj1442.15	$$⊢\chi \to PFntrCl\left(x,A,R\right)$$
16		bnj1442.16	$$⊢\chi \to QFn\left(\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
17		bnj1442.17	$$⊢\theta \leftrightarrow \left(\chi \wedge z\in E\right)$$
18		bnj1442.18	$$⊢\eta \leftrightarrow \left(\theta \wedge z\in \left\{x\right\}\right)$$
19	16	fnfund	$$⊢\chi \to \mathrm{Fun}Q$$
20		opex	$$⊢⟨x,G\left(Z\right)⟩\in \mathrm{V}$$
21	20	snid	$$⊢⟨x,G\left(Z\right)⟩\in \left\{⟨x,G\left(Z\right)⟩\right\}$$
22		elun2	$$⊢⟨x,G\left(Z\right)⟩\in \left\{⟨x,G\left(Z\right)⟩\right\}\to ⟨x,G\left(Z\right)⟩\in \left(P\cup \left\{⟨x,G\left(Z\right)⟩\right\}\right)$$
23	21 22	ax-mp	$$⊢⟨x,G\left(Z\right)⟩\in \left(P\cup \left\{⟨x,G\left(Z\right)⟩\right\}\right)$$
24	23 12	eleqtrri	$$⊢⟨x,G\left(Z\right)⟩\in Q$$
25		funopfv	$$⊢\mathrm{Fun}Q\to \left(⟨x,G\left(Z\right)⟩\in Q\to Q\left(x\right)=G\left(Z\right)\right)$$
26	19 24 25	mpisyl	$$⊢\chi \to Q\left(x\right)=G\left(Z\right)$$
27	17 26	bnj832	$$⊢\theta \to Q\left(x\right)=G\left(Z\right)$$
28	18 27	bnj832	$$⊢\eta \to Q\left(x\right)=G\left(Z\right)$$
29		elsni	$$⊢z\in \left\{x\right\}\to z=x$$
30	18 29	simplbiim	$$⊢\eta \to z=x$$
31	30	fveq2d	$$⊢\eta \to Q\left(z\right)=Q\left(x\right)$$
32		bnj602	$$⊢z=x\to pred\left(z,A,R\right)=pred\left(x,A,R\right)$$
33	32	reseq2d	$$⊢z=x\to {Q\upharpoonright }_{pred\left(z,A,R\right)}={Q\upharpoonright }_{pred\left(x,A,R\right)}$$
34	30 33	syl	$$⊢\eta \to {Q\upharpoonright }_{pred\left(z,A,R\right)}={Q\upharpoonright }_{pred\left(x,A,R\right)}$$
35	12	bnj931	$$⊢P\subseteq Q$$
36	35	a1i	$$⊢\chi \to P\subseteq Q$$
37	6	simplbi	$$⊢\psi \to RFrSeA$$
38	7 37	bnj835	$$⊢\chi \to RFrSeA$$
39	5 7	bnj1212	$$⊢\chi \to x\in A$$
40		bnj906	$$⊢\left(RFrSeA\wedge x\in A\right)\to pred\left(x,A,R\right)\subseteq trCl\left(x,A,R\right)$$
41	38 39 40	syl2anc	$$⊢\chi \to pred\left(x,A,R\right)\subseteq trCl\left(x,A,R\right)$$
42	15	fndmd	$$⊢\chi \to \mathrm{dom}P=trCl\left(x,A,R\right)$$
43	41 42	sseqtrrd	$$⊢\chi \to pred\left(x,A,R\right)\subseteq \mathrm{dom}P$$
44	19 36 43	bnj1503	$$⊢\chi \to {Q\upharpoonright }_{pred\left(x,A,R\right)}={P\upharpoonright }_{pred\left(x,A,R\right)}$$
45	17 44	bnj832	$$⊢\theta \to {Q\upharpoonright }_{pred\left(x,A,R\right)}={P\upharpoonright }_{pred\left(x,A,R\right)}$$
46	18 45	bnj832	$$⊢\eta \to {Q\upharpoonright }_{pred\left(x,A,R\right)}={P\upharpoonright }_{pred\left(x,A,R\right)}$$
47	34 46	eqtrd	$$⊢\eta \to {Q\upharpoonright }_{pred\left(z,A,R\right)}={P\upharpoonright }_{pred\left(x,A,R\right)}$$
48	30 47	opeq12d	$$⊢\eta \to ⟨z,{Q\upharpoonright }_{pred\left(z,A,R\right)}⟩=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
49	48 13 11	3eqtr4g	$$⊢\eta \to W=Z$$
50	49	fveq2d	$$⊢\eta \to G\left(W\right)=G\left(Z\right)$$
51	28 31 50	3eqtr4d	$$⊢\eta \to Q\left(z\right)=G\left(W\right)$$